The readings shared in Bluesky on 24 February 2026 are:

• Formalizing Gröbner basis theory in Lean. ~ Junyu Guo, Hao Shen, Junqi Liu, Lihong Zhi. #LeanProver #ITP #Math
• Integral curves and flows on Banach manifolds in Lean. ~ Weichen Winston Yin, Yury Kudryashov. #LeanProver #ITP #Math
• Formalization of two fixed-point algorithms in Hilbert spaces. ~ Yifan Bai, Yantao Li, Jian Yu, Jingwei Liang. #LeanProver #ITP
• Nazrin: Atomic tactics for graph neural networks for theorem proving in Lean 4. ~ Leni Aniva, Iori Oikawa, David Dill, Clark Barrett. #LeanProver #ITP
• Lean formalization of generalization error bound by Rademacher complexity. ~ Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. #LeanProver #ITP
• DSLean: A framework for type-correct interoperability between Lean 4 and external DSLs. ~ Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck. #LeanProver #ITP
• A formal correctness proof of Edmonds’ blossom shrinking algorithm. ~ Mohammad Abdulaziz, Kurt Mehlhorn. #IsabelleHOL #ITP
• Verifying the hashgraph consensus algorithm. ~ Karl Crary. #CoqProver #ITP
• Classifying 2-groups in Homotopy Type Theory. ~ Perry Hart, Owen Milner. #Agda #ITP
• Formalized run-time analysis of active learning - coalgebraically in Agda. ~ Thorsten Wißmann. #Agda #ITP
• When Agda met Vampire. ~ Artjoms Šinkarovs, Michael Rawson. #Agda #ITP #Vampire #ATP
• Haskell meets Evariste. ~ Paulo R. Pereira, Jose N. Oliveira. #Haskell #FunctionalProgramming
• Math in the age of AI. ~ Allyn Jackson. #AI4Math
• M2F: Automated formalization of mathematical literature at scale. ~ Zichen Wang et als. #AI4Math #ITP #LeanProver
• Large language model reasoning failures. ~ Peiyang Song, Pengrui Han, Noah Goodman. #LLMs #Reasoning