Readings shared February 24, 2026
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