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

This week's main thread is, once again, mathematics in the age of AI. Four reads come from the Proofs and Prompts series: Filippo A. E. Nuccio on formalisation as a manifestation of mathematical understanding, Nihar Gargava on why this is a great time to be an amateur mathematician, Isabelle Gallagher on slow maths, and Beckett Bradford on what AI does for olympiad students. Terence Tao's blog hosts two further contributions: "Mathematics has changed. Let's act like it", by Frank Calegari, and "Egoless mathematics in the AI era", by Karthik C. S., Amit Sahai and Jie Xue. Two videos complete the thread: "Mathematicians in the time of AI", by Yu Deng, and "Math 2.0", by Tao himself.

The Lean 4 section mixes formalization projects with applications. The Stacks Project has been formalized in Lean, and TechCrunch reports on Axiom Math's aim of keeping AI slop out of mathematics. Among the applications are automatic certified differentiation, the Henstock-Kurzweil path integral and operator Wick calculus, the genetic code, a two-colour zig-zag numberlink problem, and KAPPA, which checks the proofs in statistics papers with Lean 4 and language model agents. There are also new results in spectral graph theory and on Kaplansky's conjectures.

The remaining technical reads cover other proof assistants: five Isabelle/HOL entries from the Archive of Formal Proofs (including Paulson's Abel-Ruffini theorem), verified catenable deques in Rocq, and ProofStudio, which brings five proof assistants to the browser. In the Math section, Voevodsky explains the origins of univalent foundations, and Gaussianos covers the 200 TB proof of the Pythagorean triples problem.

The final section collects my own content: the Lean 4 challenges.

Lean 4

• Algebraic completeness of Feynman premeasures: The Henstock-Kurzweil path integral and operator wick calculus in Lean 4. ~ Yu. N. Berdinsky. #LeanProver #ITP #Math
• Automatic certified differentiation in Lean. ~ Ramy Shahin. #LeanProver #ITP #Math
• Axiom Math wants to keep AI slop out of mathematics. ~ Aditya Mehta. #LeanProver #ITP #AI4Math
• Kaplansky's conjectures fail for torsion-free hyperbolic groups in positive characteristic. ~ Nidhal Mghirbi, Seth Douglas. #LeanProver #ITP #AI4Math
• KAPPA: Checking the proofs in statistics papers with Lean 4 and language model agents. ~ Zihua She, Xiao Wang. #LeanProver #ITP #AI4Math
• Lemmas and conjectures in spectral graph theory. ~ Tristan Cazenave. #LeanProver #ITP #AI4Math
• Reasoning about the Genetic Code in Lean. ~ Colin T. Jones, Tyler R. Josephson. #LeanProver #ITP
• The Stacks Project, formalized in Lean. #LeanProver #ITP #AI4Math
• Two-colour zig-zag numberlink on rectangles: a forbidden-pattern characterization, a constructive polynomial-time algorithm, and a Lean verification. ~ Zzyv Zzyzek. #LeanProver #ITP

Isabelle/HOL

• Cauchy's functional equation (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• Extreme value theory (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• Finite-dimensional algebras and scalar towers. ~ Arthur Freitas Ramos, David Barros Hulak, Ruy Jose Guerra Barretto de Queiroz. #IsabelleHOL #ITP #Math
• Regular variation (in Isabelle/HOL). ~ Michikazu Hirata. #IsabelleHOL #ITP #Math
• The Abel-Ruffini theorem and the unsolvability of the quintic (in Isabelle/HOL). ~ Lawrence C. Paulson. #IsabelleHOL #ITP #Math

Rocq and other proof assistants

• ProofStudio: Five proof assistants in the browser. ~ Yutaka Nagashima. #IsabelleHOL #LeanProver #RocqProver #HOL4 #HOL_Light #ITP
• Verified purely functional catenable real-time deques. ~ Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier. #RocqProver #OCaml

Math

• Formalisation as a concrete manifestation of mathematical understanding. ~ Filippo A. E. Nuccio. #Math #Formalisation
• Pitágoras y la demostración de los 200 TB. ~ Miguel Ángel Morales. #Math #ATP #SAT_Solving
• The origins and motivations of univalent foundations (A personal mission to develop computer proof verification to avoid mathematical mistakes). ~ Vladimir Voevodsky (2014). #Math

Artificial intelligence for mathematics (AI4Math)

• Egoless mathematics in the AI era. ~ Karthik C. S., Amit Sahai, Jie Xue. #AI4Math
• It's a great time to be an amateur mathematician. ~ Nihar Gargava. #AI4Math
• Math 2.0. ~ Terence Tao. #AI4Math
• Mathematicians in the time of AI. ~ Yu Deng. #AI4Math
• Mathematics has changed. Let's act like it. ~ Frank Calegari. #AI4Math
• Slow maths. ~ Isabelle Gallagher. #AI4Math
• What does AI do for olympiad students?. ~ Beckett Bradford. #AI4Math

Lean 4 challenges (Lean4Challenge)

• Challenge 15: There exists k ∈ ℕ such that, for all n ∈ ℕ, (n + k)² ≤ 2ⁿ⁺ᵏ. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 16: For every n ∈ ℕ, n(n+1)(2n+1) is divisible by 6. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 17: Convergent sequences are bounded. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 18: Convergence of the product of convergent sequences. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 19: Convergent sequences are Cauchy sequences. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 20: If aₙ → L and M is an upper bound of aₙ, then L ≤ M. #LeanProver #LeanLang #ITP #Math #Lean4Challenge
• Solutions to Challenge 25: If the interleaving of two sequences converges to L, then both converge to L. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 26: Product of a sequence with limit zero and a bounded sequence. #LeanProver #ITP #Math #Lean4Challenge

Previous list

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