The readings shared in Bluesky on 4 February 2026 are:

• "Five-Point Haskell": Total depravity (and defensive typing). ~ Justin Le. #Haskell #FunctionalProgramming
• 'Sets' revisited: Working with a large category in Isabelle/HOL. ~ Eugene W. Stark. #ITP #IsabelleHOL
• A conversation on the future of mathematics. ~ Emily Riehl, Jesse Han, Jared Duker Lichtman. #ITP #LeanProver #Math
• Calling Lean functions as Python functions. ~ Philip Zucker. #ITP #LeanProver #Python
• Commutative algebras of series. ~ Lorenzo Clemente. #ITP #Agda #Math
• Construction-verification: A benchmark for applied mathematics in Lean 4. ~ Bowen Yang et als. #AI4Math #ITP #LeanProver
• Flow-based extremal mathematical structure discovery. ~ Gergely Bérczi, Baran Hashemi, Jonas Klüver. #AI4Math
• Formalization of non-Archimedean functional analysis 1: spherically complete spaces. ~ Yijun Yuan. #ITP #LeanProver #Math
• Hello, Haskell: Getting started in 2026. ~ Lukasz Tymoszczuk. #Haskell #FunctionalProgramming
• Irrationality of rapidly converging series: a problem of Erdős and Graham. ~ Kevin Barreto, Jiwon Kang, Sang-hyun Kim, Vjekoslav Kovač, Shengtong Zhang. #AI4Math
• LeanArchitect: Automating blueprint generation for humans and AI. ~ Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck. #AI4Math #ITP #LeanProver
• Mechanized undecidability of higher-order beta-matching. ~ Andrej Dudenhefner. #ITP #CoqProver
• Principles of programming languages. ~ Kristopher Micinski. #Programming #RacketLang
• Propositional logic proofs using Lean 4. ~ Kaue Silveira. #ITP #LeanProver #Logic #Math
• Recent advances in LLMs for mathematics. ~ Sebastien Bubeck. #AI4Math
• Semi-autonomous mathematics discovery with Gemini: A case study on the Erdős problems. ~ Tony Feng et als. #AI4Math #ITP #LeanProver
• The Leibniz adjunction in homotopy type theory, with an application to simplicial type theory. ~ Tom de Jong, Nicolai Kraus, Axel Ljungström. #ITP #Agda
• The evolution of a Lean programmer. #ITP #LeanProver #FunctionalProgramming