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

This week's main thread is the role of AI in mathematical practice and research ethics. Most of the AI4Math reads come from the Proofs and Prompts series: Thomas Sinclair on free inquiry, Hendrik De Bie on AI statements in mathematics papers, Michel Schellekens on trustworthy AI, Thomas Koberda and Alex Kontorovich on the dialectical theorem, and Benjamin Braun on how mathematics is being transformed. Lawrence Paulson adds a related reflection on plagiarism in the age of AI.

The Lean 4 section is dominated by new formalizations: the disproof of Ramaekers's conjecture, a counterexample to Erdős problem 108, the eleven-variable Vasc inequality, flag algebras, the irrationality measure of the logarithm of a rational number, pedigree polytopes and term relation algebras. Also worth a look is "How to formalize all of mathematics", by Avigad, Buzzard, Commelin, Degenne, Morrison, Nash and Topaz.

The final sections collect my own content: the Lean 4 challenges (in English and in Spanish) and a post on the real numbers in Spanish.

Lean 4

• A counterexample to Erdős problem 108 via arc graphs. ~ Jensen Kohlmeyer, Liam Kruer. #LeanProver #ITP #Math
• A Lean formalisation of the disproof of Ramaekers's conjecture. ~ Jeremy Tan. #LeanProver #ITP #Math
• An efficient, Lean 4 verified necessary and sufficient condition for membership in pedigree polytopes. ~ T.S. Arthanari. #LeanProver #ITP #AI4Math
• Exact rational certificates and a Lean formalization of the eleven-variable Vasc inequality. ~ Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, Xiao-Shan Gao. #LeanProver #ITP
• Formalizing flag algebras in Lean. ~ Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum, Hongseok Yang. #LeanProver #ITP #AI4Math
• How to formalize all of mathematics. ~ Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz. #LeanProver #ITP #AI4Math
• Lean 4 for mathematicians: a teacher's guide. #LeanProver #ITP #Math
• Mechanizing term relation algebras: the basic theory. ~ Jacopo Angeli. #LeanProver #ITP
• The irrationality measure of the logarithm of a rational number is 2. ~ Dan Brown. #LeanProver #ITP #Math

Artificial intelligence for mathematics (AI4Math)

• Free inquiry in mathematics. ~ Thomas Sinclair. #AI4Math
• On AI statements in mathematics papers. ~ Hendrik De Bie. #AI4Math
• On our existential crisis and trustworthy AI. ~ Michel Schellekens. #AI4Math
• Plagiarism in the age of AI. ~ Lawrence Paulson. #AI
• The dialectical theorem. ~ Thomas Koberda, Alex Kontorovich. #AI4Math
• Transforming mathematics. ~ Benjamin Braun. #AI4Math

Lean 4 challenges (Lean4Challenge)

• Challenge 1: Prove in Lean 4 that the sequence 1/n converges to 0. #LeanProver #ITP #Math #Lean4Challenge
• Challenge 2: The sequence 1, -1, 1, -1,... is not convergent. #LeanProver #ITP #Math #Lean4Challenge

Content in Spanish

Lean 4 challenges (RetoLean4)

• Enunciado del reto 23 de Lean 4: La sucesión constante aₙ = L converge a L. #RetoLean4 #LeanProver #ITP #Math
• Soluciones 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

Mathematics

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

Previous list

• Weekly reads: Oct 5 – Oct 11, 2026. #AI4Math #Autoformalization #CAS #FunctionalProgramming #Haskell #IsabelleHOL #ITP #LeanProver #Logic #Math #RetoLean4 #RocqProver