The readings shared in Bluesky on 24 March 2026 are:

• Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math
• The spectral comb and the Riemann hypothesis: A proof via fixed-point theory. ~ Engin Atik. #LeanProver #ITP #Math
• Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. #LeanProver #ITP #Math
• Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. ~ Vasily Ilin. #LeanProver #ITP
• Rado's radical reflections. ~ Rado Kirov. #LeanProver #ITP #FunctionalProgramming
• OpenGauss: an open source, state of the art autoformalization harness. #AI4Math #LeanProver #ITP #Autoformalization
• Verso: a platform for writing documents, books, course materials, and websites with Lean. #LeanProver
• Lebesgue-Stieltjes integral (in Isabelle/HOL). ~ Yosuke Ito. #IsabelleHOL #ITP #Math
• Sorted rewriting, conditional rewriting, and logically constrained rewriting (in Isabelle/HOL). ~ Akihisa Yamada. #IsabelleHOL #ITP
• A formal embedding for assessing the complexity of model consistency. ~ Romain Pascual et als. #IsabelleHOL #ITP
• Liberator: A drag-and-drop visual programming environment for Haskell. ~ Miles Berry. #Haskell #FunctionalProgramming