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