Here are the reads I shared on Mastodon this past week:

1. Lean 4

• A constructive ATLAS of finite simple groups in Lean. ~ Gerald Höhn. #LeanProver #ITP #AI4Math
• A Lean formalization of the Hamilton-Perelman proof of the three-dimensional Poincaré conjecture. ~ Ziyang Qin, Yuan Liao, Ayush Khaitan, Bennett Chow. #LeanProver #ITP
• Formalising linear elliptic PDE theory in Lean 4. ~ Alejandro José Soto Franco, Kobe Marshall-Stevens. #LeanProver #ITP #Math
• Formalization of the Poincaré Conjecture in Lean 4. ~ PKU AI for Math team. #LeanProver #ITP #Math
• Formalize everything, now! ~ Justin Asher. #LeanProver #ITP #AI4Math
• Formalizing Carleson's theorem in Lean. ~ Lars Becker et als. #LeanProver #ITP #Math
• New proofs of weak normalization for propositional logic. ~ S P Suresh. #LeanProver #ITP #Logic
• Papers with Lean: arXiv papers that use Lean. #LeanProver #ITP
• Proving at scale for universal algebra. ~ João Araújo, Jan Hula, Mikoláš Janota, Edmond W. H. Lee, Bartosz Naskrecki. #LeanProver #ITP #AI4Math
• Sage: Formalization with semantic correction. ~ Thomas Hirtz, Farzad Jafarrahmani, Abdelmouksit Sagueni, Xiang Zhou, Wengping Deng, Liang Zhang. #LeanProver #ITP #AI4Math
• The Odlyzko–Poonen conjecture on irreducibility of random polynomials. ~ Constantin Kogler. #LeanProver #ITP #AI4Math
• What did the Lean proof of Fermat's Last Theorem formalize? ~ Justin Asher. #LeanProver #ITP #AI4Math

2. Isabelle/HOL

• Proofs without nominals: Gödel's ontological argument, its shallow embedding, and the open questions of the Monatshefte Notes. ~ Christoph Benzmüller. #LeanProver #IsabelleHOL #ITP

3. Artificial intelligence for mathematics (AI4Math)

• AI for mathematical problems: an invitation for mathematicians. ~ Matthew Colbrook et als. #AI4Math
• AI solves a ‘holy grail’ problem from probability theory. ~ Manon Bischoff. #AI4Math
• AIM, explained (Explanations of open applied mathematics). ~ Matthew Colbrook et als. #AI4Math
• AIM: an invitation to explore mathematics together. ~ Matthew Colbrook. #AI4Math
• Applied mathematics has met the machine before. ~ Denys Dutykh. #AI4Math
• Can AI truly prove anything? ~ Stepan Nesterov. #AI4Math
• If math is more than proof, we need to better celebrate the rest of it. ~ Grant Sanderson. #AI4Math
• Only Anatevka: the mathematical community's values, its incentives, and LLMs. ~ Ethan Sussman. #AI4Math
• Responsible release of AI-generated mathematics. ~ Advisory Group on Mathematics and Artificial Intelligence. #AI4Math
• To grieve, or not to grieve? (Mathematics and AI). ~ Kevin Buzzard. #AI4Math
• Why I became a professional mathematician. ~ Frank Vallentin. #AI4Math
• YAPOAI (Yet Another Post on AI): AI, understanding, and mathematical work. ~ Najib Idrissi. #AI4Math

4. Other topics

• Free math textbooks from university mathematicians. #Math
• Teaching Haskell in the age of LLMs, part 1: ban or embrace? ~ Vladislav Zavialov. #Haskell #FunctionalProgramming #LLMs

5. Content in Spanish

5.1 Lean 4 challenges (RetoLean4)

• #RetoLean4: Soluciones del reto 17 (Las sucesiones convergentes están acotadas). #LeanProver #ITP #Math
• #RetoLean4: Soluciones del reto 20 (Si aₙ → L y M es una cota superior de aₙ, entonces L ≤ M). #LeanProver #ITP #Math
• #RetoLean4: Enunciado del reto 21 (Las subsucesiones tienen el mismo límite que la sucesión). #LeanProver #ITP #Math

5.2 Reviews of AI4Math posts

• Reseña de «AI solves a ‘holy grail’ problem from probability theory». #AI4Math
• Reseña de «AIM: an invitation to explore mathematics together». #AI4Math
• Reseña de «Applied mathematics has met the machine before». #AI4Math
• Reseña de «Can AI truly prove anything?» #AI4Math
• Reseña de «Only Anatevka: the mathematical community's values, its incentives, and LLMs». ~ Ethan Sussman. #AI4Math
• Reseña de «Responsible release of AI-generated mathematics». #AI4Math
• Reseña de «To grieve, or not to grieve? (Mathematics and AI)». #AI4Math
• Reseña de «If math is more than proof, we need to better celebrate the rest of it». #AI4Math
• Reseña de «Why I became a professional mathematician». #AI4Math
• Reseña de «YAPOAI (Yet Another Post on AI): AI, understanding, and mathematical work». #AI4Math

6. Previous list

• Weekly reads: 21-27 September, 2026 #AI4Maht #Agda #ITP #IsabelleHOL #LeanProver #LogicProgramming #Math #Prolog #RocqProver