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

This week's main thread is, once again, the future of mathematics in the age of AI, now with two community reports: "The mathematical sciences in an AI-enabled world", by Christoph Reisinger et al., and the report of the "Summit on math research in the age of AI". The Proofs and Prompts series contributes Tim Gehrunger on AI reviews, Patrick Morris on whether we should stop writing papers and Alonso Castillo-Ramirez on AI and the correction of the mathematical literature. Terence Tao's blog hosts Gireeja Ranade on education and a public goods problem, Celina Zhao asks in Science whether AI proofs can be trusted, and Lauren Williams offers a nuanced assessment of AI's ability to solve math problems in a talk about First Proof.

The Lean 4 section is dominated by large-scale formalization: Axiom has formalized the classification of finite simple groups, the longest proof in the history of mathematics. It also includes the PaperFormalizer approach to autoformalizing research papers, the degenerations of Jordan algebras and the formalization of reasoning about the genetic code.

The Isabelle/HOL section brings five new entries to the Archive of Formal Proofs: the irrationality of ζ(5), modular forms, a countable version of Dilworth's theorem, the travelling salesman problem via dynamic programming and the consistency of NK with infinity and choice. A Spanish read on real numbers by Esteban Martínez completes the list.

The final section collects my own content: the Lean 4 challenges on sequences and limits.

Lean 4

• Degenerations of Jordan algebras. ~ Victor Bovdi, Ivan Kaygorodov, Yury Popov, Azamat Saydaliyev, Yury Volkov. #LeanProver #ITP #Math
• Formalizing the Enormous Theorem. #LeanProver #ITP #AI4Math #AI #Math
• PaperFormalizer: Author-in-the-loop autoformalization of research papers in Lean. ~ Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet. #LeanProver #ITP #AI4Math #Autoformalization
• Reasoning about the genetic code in Lean. ~ Colin T. Jones, Tyler R. Josephson. #LeanProver #ITP
• The classification of finite simple groups, formalized in Lean. #LeanProver #ITP #AI4Math #AI #Math

Isabelle/HOL

• Countable infinite version of Dilworth's theorem (in Isabelle/HOL). ~ Fabián Fernando Serrano Suárez, Thaynara Arielly de Lima, Mauricio Ayala-Rincón. #IsabelleHOL #ITP #Math
• HOL in HOL over a set-theoretic universe: consistency of NK with infinity and choice. ~ Christoph Benzmüller, Daniel Kirchner. #IsabelleHOL #ITP #Logic
• Modular forms (in Isabelle/HOL). ~ Manuel Eberl, Anthony Bordg, Lawrence C. Paulson, Wenda Li. #IsabelleHOL #ITP #Math
• The irrationality of ζ(5) (in Isabelle/HOL). ~ Alex Raymond Hyman. #IsabelleHOL #ITP #Math
• Travelling Salesman via dynamic programming (in Isabelle/HOL). ~ Maksym Bortin. #IsabelleHOL #ITP

Artificial intelligence for mathematics (AI4Math)

• AI is shaking up math. But can its proofs be trusted?. ~ Celina Zhao. #AI4Math
• AI reviews are the new normal. ~ Tim Gehrunger. #AI4Math
• AI, mathematics, education, and a public goods problem. ~ Gireeja Ranade. #AI4Math
• Could AI help correct the mathematical literature?. ~ Alonso Castillo-Ramirez. #AI4Math
• First Proof: A nuanced assessment of AI's ability to solve math problems. ~ Lauren Williams. #AI4Math
• Let's stop writing papers…. ~ Patrick Morris. #AI4Math
• Report of "Summit on math research in the age of AI". #AI4Math
• The mathematical sciences in an AI-enabled world (Opportunities, risks and community needs). ~ Christoph Reisinger, Rachel Bearon, Thomas Bloom, Jennifer Gaskell, David Leslie, Zubin Siganporia. #AI4Math

Mathematics

• ¿Qué son los números reales? IV. ~ Esteban Martínez. #Math

Lean 4 challenges (Lean4Challenge)

• Solutions to Challenge 8: Uniqueness of the limit of convergent sequences. #LeanProver #ITP #Math #Lean4Challenge
• Solutions to Challenge 10: If aₙ → L with L ≠ 0, then |aₙ| ≥ |L|/2 eventually. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 11: If aₙ converges to L, then |aₙ| converges to |L|. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 12: If aₙ → L, bₙ → M and L < M, then eventually aₙ < bₙ. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 13: Reverse triangle inequality: ||x| - |y|| ≤ |x - y|. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 14: For all n ∈ ℕ, 2n + 9 ≤ 2ⁿ⁺⁴. #LeanProver #ITP #Math #Lean4Challenge
• Solutions to Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (2nd version). #LeanProver #ITP #Math #Lean4Challenge
• Challenge 25: If the interleaving of two sequences converges to L, then both converge to L. #LeanProver #ITP #Math #Lean4Challenge

Previous list

• Weekly reads: Oct 19 – Oct 25, 2026. #AI #AI4Math #ITP #Lean4Challenge #LeanProver #Logic #LogicProgramming #Math #Prolog #RetoLean4