The readings shared in Mastodon on 17 August 2026 are:

• A computer-assisted proof of Sendov’s conjecture. ~ Lech Mazur. #LeanProver #ITP #AI4Math
• A formalization of the Laplace transform and its inversion in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. #LeanProver #ITP #Math
• A proof of the Dittert conjecture in dimension 4 via an exact constrained sum-of-squares certificate. ~ Jinhui Li, Beibei Xiong, Zhengfeng Yang. #LeanProver #ITP #Math
• AnnalsChallenge is a collection of formalised statements of recent important theorems. These theorems are the main results of papers published in the Annals of Mathematics in the 2020s. The statements are written in Lean 4, using Mathlib. #LeanProver #ITP #Math
• Banach lattices and phase retrieval: A case study for the use of AI in mathematics. ~ Jaume de Dios Pont, Lukas Liehr, David Muñoz-Lahoz, Mitchell A. Taylor, Pedro Tradacete. #LeanProver #ITP #AI4Math
• Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. #LeanProver #ITP #AI4Math
• Dilatations of categories, via their lean formalization. ~ Arnaud Mayeux. #LeanProver #ITP
• FormaTheoria: Constructing large-scale lean theories from mathematical literature (Toward the formalization of the classification of finite simple groups). ~ Tianjiao Nie, Ao Zhang, Yusen Tang, Damiano Testa, Shing-Tung Yau, Peng Li, Yuan Zhou. #LeanProver #ITP #AI4Math
• From the Dirichlet integral to Lobachevsky's formula: a formalization in Lean 4. ~ Daniel Goldberg, Antoine Vinciguerra. #LeanProver #ITP #Math
• Grothendieck's theorem for Bessel sequences. ~ Lukas Liehr, Mitchell A. Taylor, Peiyang Yu. #LeanProver #ITP #Math
• Is this the end of handwritten math? Introducing Lean. ~ Ank Yog. #LeanProver #ITP #Math
• Lean 4.33.0 is live! #LeanProver #ITP
• Les mathématiques du secondaire français, démontrées en Lean. ~ Michel Hua. #LeanProver #ITP #Math #AI4Math
• The Annals Challenge. ~ Kevin Buzzard. #LeanProver #ITP #Math
• The Banach lattice Lean library. ~ David Muñoz-Lahoz. #LeanProver #ITP #Math
• The Gaussian code bridge: E8 over Z[i], the extended Hamming code, and a four-bit information layer. ~ Stefan Hamann. #LeanProver #ITP
• The Lean Kernel Arena presents, tests and benchmarks proof checkers for the Lean Theorem Prover. #LeanProver #ITP
• The set of primes is supernatural: a Lean formalization of the statement of the conjecture. ~ A. Mayeux. #LeanProver #ITP #Math
• Vero: Can AI agents build formally verified software repositories? ~ Zhe Ye et als. #LeanProver #ITP #FormalVerification
• CAPRI: Contract-aware proof repair for Isabelle. ~ Jim Woodcock, Gabriel Leite, Augusto Sampaio, Ran Wei. #IsabelleHOL #ITP #LLMs
• First-order methods for smooth convex optimization in Isabelle/HOL. ~ Feier Lyu. #IsabelleHOL #ITP #Math
• Machine-checked dual-write recovery from a committed log. ~ Andreas Andreakis. #IsabelleHOL #ITP
• A SAT attack on Tarski's high school algebra problem. ~ Bernardo Subercaseaux, Benjamin Przybocki. #ATP #SATsolvers #Math
• Proofs and prompts (a communal blog about mathematics in the age of AI). #AI4Math
• The end of an era in mathematical research. ~ Alonso Castillo-Ramirez. #AI4Math
• The end of mathematics. ~ Daniel Litt. #AI4Math
• The path to mathematical superintelligence. ~ Tudor Achim. #AI4Math
• The question of reasoning traces. ~ Segev Gonen Cohen. #AI4Math
• TheoremDB: A public workspace for machine mathematics. #AI4Math #LeanProver
• What I feel like when I work with an AI. ~ Shmuel Weinberger. #AI4Math
• What sort of maths are LLMs good at? ~ Timothy Gowers. #AI4Math
• Writing mathematics in the age of AI. ~ Main Hairer. #AI4Math
• Solving AoC with Haskell. ~ Asliddin Abdivasiyev. #Haskell #FunctionalProgramming
• #RetoLean4: Retos de demostración en Lean 4. #LeanProver #ITP #Math
• #Calculemus: Demostraciones con Lean 4 de "La sucesión 1/n converge a 0". #LeanProver #Math