Here are the 42 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. Most of the AI4Math reads come from the Proofs and Prompts series: the question of who will become the new mathematicians of Math 2.0 and the responses it prompted (Álvaro Lozano-Robledo), a critique of the mathematical economy (Álvaro Gutiérrez), András Juhász on public good, credit and education, Marcus Zibrowius on being disgusted by AI, David A. Madore's letter to a worried student, Dave Anderson on the dark forest, Helmut Hofer on who will lead mathematical AI, and "Mathematics of the future", by Pavel Etingof et al. Terence Tao's blog hosts two further perspectives, by Tristan Buckmaster and Francesco Maggi, and Tao himself proposes an experimental AI-math challenge on Siegel zeroes. Konstantin Kakaes discusses in Quanta Magazine the AI proof of the quasi-Riemann hypothesis, and the REUF2F benchmark evaluates coding agents on formalized undergraduate research problems.

The Lean 4 section combines new formalizations with reflections on the system itself: the formalization of model theory by Yunus Maranki, the real interpolation theorem for the Carleson project, the falsity of Isaac's condition (TU) and the irrationality exponent of the lemniscate period. Also worth a look are "Maestro", on agentic formal proof development, "Reflections on trusting Lean", by Lorenzo Bresolin and Marcello Mamino, and the values of Mathlib. A reading on Prolog and logic programming, "Simply logical", completes the technical part.

The final sections collect my own content: the Lean 4 challenges (in English and in Spanish) and my reviews of four of the AI4Math posts.

Lean 4

• Formalization of model theory in Lean. ~ Yunus Maranki. #LeanProver #ITP #Logic #Math
• Formalization of the real interpolation theorem for the Carleson project. ~ Jim Portegies, Michael Rothgang. #LeanProver #ITP #Math
• Isaac's condition (TU) is false. ~ Ralf Stephan. #LeanProver #ITP #Math
• Maestro: Agentic formal proof development by coordination. ~ Haoyu Li et al. #LeanProver #ITP #AI4Math
• Mathlib's values. #LeanProver #ITP
• Reflections on trusting Lean. ~ Lorenzo Bresolin, Marcello Mamino. #LeanProver #ITP #Logic #Math
• The irrationality exponent of the lemniscate period: A determinant proof with a Lean 4 formalization. ~ Gregory V. Chudnovsky. #LeanProver #ITP #AI4Math

Logic programming

• Simply logical - The first three decades. ~ Peter Flach, Kacper Sokol, Jan Wielemaker. #Prolog #LogicProgramming

Artificial intelligence for mathematics (AI4Math)

• A critique of the mathematical economy. ~ Álvaro Gutiérrez. #AI4Math
• A response to “Who will become the new mathematicians of Math 2.0?”. ~ Álvaro Lozano-Robledo. #AI4Math #AI #Math
• AI and mathematics: public good, credit, and education. ~ András Juhász. #AI4Math #AI #Math
• AI proved the quasi-Riemann hypothesis. What happens now?. ~ Konstantin Kakaes. #AI4Math
• An experimental AI-math challenge: using tenth discriminant bounds to explore arguments ruling out Siegel zeroes. ~ Terence Tao. #AI4Math
• Disgusted by AI?. ~ Marcus Zibrowius. #AI4Math
• Letter to a worried student. ~ David A. Madore. #AI4Math
• Mathematics in the dark forest. ~ Dave Anderson. #AI4Math
• Mathematics is a subject for the young. ~ Tristan Buckmaster. #AI4Math
• Mathematics of the future. ~ Pavel Etingof et al. #AI4Math
• Recommendations on the use of AI for PhD students and supervisors. #AI4Math
• REUF2F: Benchmarking coding agents on formalized undergraduate research problems. ~ Zeyu Zheng et al. #AI4Math
• The power of beauty and elegance. ~ Márton Balázs. #AI4Math
• Thinking hard above AI. ~ Benjamin Merlin Bumpus. #AI4Math
• Who will become the new mathematicians of Math 2.0?. #AI4Math
• Who will lead mathematical AI?. ~ Helmut H. W. Hofer. #AI4Math
• Will it be a golden age or a dark age for mathematics (and science)?. ~ Francesco Maggi. #AI4Math

Lean 4 challenges (Lean4Challenge)

• Challenge 3: If aₙ converges to L, then 2aₙ converges to 2L. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 4: There are infinitely many prime numbers. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 5: 5²ⁿ - 2³ⁿ is divisible by 17. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 6: If aₙ and cₙ converge to L and aₙ ≤ bₙ ≤ cₙ for all n, then bₙ converges to L. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 7: The composition of injective functions is injective. #LeanProver #ITP #Math #Lean4Challenge
• Solutions to Challenge 23: The constant sequence aₙ = L converges to L. #Lean4Challenge #LeanProver #ITP #Math
• Challenge 24: The sequence 1, -1, 1, -1,... is not convergent (using Challenge 22). #Lean4Challenge #LeanProver #ITP #Math

Reviews

• Review of «Disgusted by AI?». #AI4Math
• Review of «Mathematics is a subject for the young». #AI4Math #AI #Math
• Review of «Mathematics of the future». #AI4Math
• Review of «Towards a world mathematical commons». #AI4Math #LeanProver #ITP #AI #Math

Content in Spanish

Lean 4 challenges (RetoLean4)

• Reto 24 de Lean 4: La sucesión 1, -1, 1, -1,... no es convergente (usando el Reto 22). #RetoLean4 #LeanProver #ITP #Math
• Soluciones del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. #RetoLean4 #LeanProver #ITP #Math

Reviews (Reseñas)

• Reseña de «Disgusted by AI?». #AI4Math
• Reseña de «Mathematics is a subject for the young». #AI4Math #AI #Math
• Reseña de «Mathematics of the future». #AI4Math
• Reseña de «Towards a world mathematical commons». #AI4Math #LeanProver #ITP #AI #Math

Previous list

• Weekly reads: Oct 12 – Oct 18, 2026. #AI #AI4Math #ITP #Lean4Challenge #LeanProver #Math #RetoLean4