All the math we will not see. ~ Alessandro Della Corte. proofsandprompts.com/2026/09/24/a... #AI4Math

Formalization of Harder-Narasimhan theory. ~ Yijun Yuan. arxiv.org/abs/2509.19632 #LeanProver #ITP #AI4Math

Gödel's and Scott's variants of the ontological argument in Lean 4. ~ Christoph Benzmüller. arxiv.org/abs/2609.268... #LeanProver #ITP #AI4Math

AI and mathematical research. ~ Claudia Alfes, Thomas Nikolaus, Andreas Thom. ai.math.ms/en/research/ #AI4Math

Navigating the AI crisis: a humble guide for students. ~ Tarik Aougab. proofsandprompts.com/2026/09/23/n... #AI4Math

#Vestigium: Lista de usos y expectativas de la IA en matemáticas. jaalonso.github.io/vestigium/po... #AI4Math

New math + AI developments in fluid mechanics. ~ Javier Gomez-Serrano. youtu.be/TcEefrWrddA #AI4Math

ProofForum: Keeping AI-generated mathematics human. ~ Marco Trombetti. proofsandprompts.com/2026/09/22/p... #AI4Math

El miedo al lado oscuro de la IA en la comunidad matemática. ~ Anabel Forte Deltell. theconversation.com/el-miedo-al-... #AI4Math

Verifying numerical methods with Isabelle/HOL. ~ Dustin Bryant, Jonathan Julian Huerta y Munive, Simon Foster. arxiv.org/abs/2511.20550 #IsabelleHOL #ITP #AI4Math

¿Realmente ha resuelto OpenAI el "problema matemático del milenio" de Navier-Stokes? ~ Víctor Javier Llorente Lázaro. theconversation.com/realmente-ha... #AI4Math

The scientific debate over AI in mathematics. ~ Oswaldo Royett. www.oswaldosrm.com/single-post/... #AI4Math

Readings shared: 14-20 September, 2026. jaalonso.github.io/vestigium/po... #AI #AI4Math #Emacs #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math #RocqProver

Lean-certified infinite counterexamples to written on the Wall II Conjecture 194. ~ Cameron Beeley. arxiv.org/abs/2609.191... #LeanProver #ITP #AI4Math

Descriptive complexity in Lean: completeness by first-order reductions. ~ Pierre Senellart, Anton Gnatenko. arxiv.org/abs/2609.182... #LeanProver #ITP #AI4Math

Where will all the papers go? ~ David Craven. proofsandprompts.com/2026/09/19/w... #AI4Math

Existential risk from AI: an exposition for mathematicians. ~ Xiaoyu He. alkjash.github.io/ai-risk/ #AI4Math

Two responses to "A severe misalignment of AI in mathematics". ~ Timothy Nguyen, M. Levent Doğan. proofsandprompts.com/2026/09/18/t... #AI4Math

Formalization of Sullivan's no wandering domains theorem in Lean. ~ Ziang Li, Yusheng Luo. arxiv.org/abs/2609.160... #LeanProver #ITP #AI4Math

Building open models for the mathematical community (An invitation from SAIR Foundation). sair.foundation/open-math-mo... #AI4Math