Readings shared February 9, 2026
The readings shared in Bluesky on 9 February 2026 are:
- A Lean 4 formalization of the gaussian free field in d=4 and proof of the Osterwalder-Schrader axioms. ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. #ITP #LeanProver
- Accelerating mathematics. ~ Kevin Buzzard. #AI4Math #ITP #LeanProver
- CSLib: The Lean computer science library. ~ Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, Sorrachai Yingchareonthawornchai. #ITP #LeanProver #CompSci
- Fel's conjecture on syzygies of numerical semigroups. ~ Evan Chen et als. #ITP #LeanProver #Math
- Formalization of Weyl’s law and its implementation into Lean code. ~ Zhibin Huang. #ITP #LeanProver #Math
- Inequalities for octad weights in M24 a computational framework formalized in Lean 4. ~ Yoshihiro Hasegawa. #ITP #LeanProver
- Statistical learning theory in Lean 4: Empirical processes from scratch. ~ Yuanhe Zhang, Jason D. Lee, Fanghui Liu. #ITP #LeanProver
- Towards trustworthy AI results using evidence structures: From certificates to argumentation frameworks. ~ Shawn Bowers1, Bertram Ludäscher. #ITP #LeanProver
- Formal P‑category theory and normalisation for simple type theory. ~ David George Berry. #ITP #RocqProver
- Evaluating Large Language Models on solved and unsolved problems in graph theory: Implications for computing education. ~ Adithya Kulkarni, Mohna Chakraborty, Jay Bagga. #AI4Math