Here are the 38 reads I shared on Mastodon this past week.

This week's main thread is the impact of AI on mathematics. Terence Tao ("Math 2.0"), Jeremy Avigad, Christian Szegedy and Quanta Magazine each ask where the field is heading, and Thomas Hales discusses the reliability of Lean and AI-generated proofs. A related theme in the Lean 4 section is autoformalization: Scott Armstrong argues it is now very easy and releases a collection of skills for Codex and Claude Code, and there is an AI-assisted formalization of the Poincaré conjecture. Also worth a look is the online edition of Software Foundations in Lean.

The rest covers Isabelle/HOL (geometry in the AFP, Isabelle/ML metaprogramming, and teaching logic), a Rocq certification result for polyhedra, and a classic Haskell textbook. The final section collects content in Spanish: a teaching guide on Lean 4, the Lean 4 challenges and reviews of some of the AI4Math posts above.

Lean 4

• A Lean 4 framework for the radii polynomial method. ~ Fengyang Wang. #LeanProver #ITP #Math
• Advancing mathematics research with AI-driven formal proof search. ~ George Tsoukalas et al. #LeanProver #ITP #AI4Math
• AIProver: agentic auto-formalization of mathematical research via certificate-driven evolving harness. ~ Prithwish Jana et al. #LeanProver #ITP #AI4Math
• An AI-assisted formalization of the Poincaré conjecture. ~ Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong. #LeanProver #ITP #AI4Math
• Autoformalization is now very easy. ~ Scott Armstrong. #LeanProver #ITP #AI4Math #Autoformalization
• Erdős 374: classical square products of factorials (in Lean 4). ~ Alexander. #LeanProver #ITP #Math
• LeanAutoformalizationSkills: A collection of skills for using Codex or Claude Code to formalize mathematics in Lean 4. ~ Scott Armstrong. #LeanProver #ITP #AI4Math #Autoformalization
• Software Foundations in Lean. ~ Benjamin Pierce et al. #LeanProver #ITP
• Sound and complete solving for multi-width parametric bitvectors via principled reductions. ~ Siddharth Bhat et al. #LeanProver
• Toward a Lean formalization of analog computing with microwaves. ~ Matteo Nerini, Xuekang Liu, Bruno Clerckx. #LeanProver #ITP
• We live in the dependently typed future now. ~ Stephen Diehl. #LeanProver #ITP #AI4Math
• What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI. ~ Thomas Hales. #LeanProver #ITP #AI4Math
• ZFLean: a Lean 4 library for doing core mathematics inside Mathlib's model of ZFC set theory. ~ Vincent Trélat, Matteo Pouillat. #LeanProver #ITP #Math
• ZFLean: a framework for set-level mathematics in Lean. ~ Vincent Trélat, Matteo Pouillat. #LeanProver #ITP #Math

Isabelle/HOL

• A first introduction to Isabelle/ML metaprogramming: automatic estimation of polynomial degrees. ~ Jonas Bayer, Anna Danilkin, Marco David, Annie Yao. #IsabelleHOL #ITP
• Mathematical proof assistants for teaching logic: the LogiKEy methodology. ~ Christoph Benzmüller, David Fuenmayor, Luca Pasetto. #IsabelleHOL #ITP #Logic
• Steiner's line theorem in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• The Steiner deltoid as the tangent envelope of Wallace-Simson lines in Isabelle/HOL. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math

Rocq

• Formally certifying the vertex set of a polyhedron faster than informal enumeration. ~ Xavier Allamigeon, Yazid Id-Sahra, Pierre-Yves Strub. #RocqProver #ITP #Math

Artificial intelligence for mathematics (AI4Math)

• Agentic approach to computer algebra systems. ~ Bartosz Naskręcki et al. #AI4Math #CAS
• Could AI help mathematics escape the meritocracy trap?. ~ Anonymous mathematician in the United States. #AI4Math
• Is AI the end of math as we know it?. ~ Jordana Cepelewicz. #AI4Math
• Is mathematics over, or just graduating?. ~ Christian Szegedy. #AI4Math
• Math 2.0. ~ Terence Tao. #AI4Math
• Navigating the risks of AI in academia. ~ Sahana Balasubramanya. #AI4Math
• On OpenAI’s release of mathematical results. ~ Advisory Group on Mathematics and Artificial Intelligence. #AI4Math
• Solving open research problems together (Mathematicians and Muse Spark collaborate on six research papers). ~ Meata AI. #AI4Math
• The future of mathematics. ~ Jeremy Avigad. #AI4Math
• What should we tell our students?. ~ Álvaro Lozano-Robledo. #AI4Math

Haskell

• Online edition of "Haskell: the craft of functional programming". ~ Simon Thompson. #Haskell #FunctionalProgramming

Content in Spanish

Teaching Lean 4

• Lean 4 para matemáticos: guía docente. #LeanProver #ITP #Math

Lean 4 challenges (RetoLean4)

• Enunciado del reto 22 de Lean 4: Si una sucesión tiene dos subsucesiones con límites distintos, entonces la sucesión no es convergente. #RetoLean4 #LeanProver #ITP #Math
• Soluciones del reto 21 de Lean 4: Las subsucesiones tienen el mismo límite que la sucesión. #RetoLean4 #LeanProver #ITP #Math

Artificial intelligence for mathematics (AI4Math)

• Debate sobre Matemáticas e IA: IA en EDPs. ~ Javier Gómez Serrano. #AI4Math
• Reseña de «Is AI the end of math as we know it?». #AI4Math
• Reseña de «Is mathematics over, or just graduating?». #AI4Math
• Reseña de «Navigating the risks of AI in academia». #AI4Math
• Reseña de «The future of mathematics». #AI4Math

Previous list

• Weekly reads: Sep 28 – Oct 4, 2026. #AI4Math #Agda #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Prolog #RocqProver