#ai4math — Public Fediverse posts

Changes in the classroom in the AI Era. ~ Benjamin Jaye, Galyna V. Livshyts. https://proofsandprompts.com/2026/08/19/changes-in-the-classroom-in-the-ai-era/ #AI4Math

A proof of the Regts–Sevenster conjecture, formalized. ~ William Whistler. https://github.com/WillWhistler/Regts-Sevenster #LeanProver #ITP #AI4Math

A Lean formalization of the main theorem of the paper "Low-rank univariate sum of squares has no spurious local minima". ~ Chenyang Yuan. https://github.com/yuanchenyang/lean_low_rank_univariate_sos #LeanProver #ITP #AI4Math

Erdős problem #501 in Lean 4. ~ Elliot Glazer. https://github.com/elliotglazer/erdos501 #LeanProver #ITP #Math #AI4Math

Response to "The AI dissenter viewpoint". ~ Anatoly Vitold Stankyavichyus. https://proofsandprompts.com/2026/08/20/response-to-the-ai-dissenter-viewpoint/ #AI4Math

Formal verification of Romanov's triplet logic: A verified filter for sliding-window 3-CNF with application to structured formulas. ~ Dmitry V. Alexandrov. https://arxiv.org/abs/2608.18445v1 #RocqProver #ITP #AI4Math

On protecting mathematics from LLM companies’ monopoly. ~ Tian Lan. https://proofsandprompts.com/2026/08/18/on-protecting-mathematics-from-llm-companies-monopoly/ #AI4Math

Human mathematics in the age of reasoning machines. ~ Akshay Venkatesh. https://www.math.ias.edu/~akshay/research/ReimaginingDetails.pdf #AI4Math

On the existence problem of regular Gabor frames. ~ Jaume de Dios Pont, Lukas Liehr, Mitchell A. Taylor. https://arxiv.org/abs/2606.26052 #LeanProver #ITP #AI4Math

Stable phase retrieval for spans of independent random variables. ~ Pedro Abdalla, Jaume de Dios Pont, João P. G. Ramos, Mitchell A. Taylor. https://arxiv.org/abs/2607.06693 #LeanProver #ITP #AI4Math

Lean formalization of bounded gaps between primes. ~ Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie. https://primegaps.axiommath.ai/ #LeanProver #ITP #AI4Math

A Lean 4 formalization of Pick's theorem, the polygonal Jordan curve theorem, the full Jordan curve theorem, and Radó's theorem. ~ Rado Kirov. https://github.com/rkirov/jordan_pick #LeanProver #ITP #AI4Math

Palomar: A public registry of Lean-verified mathematics. https://palomar-registry.org/ #LeanProver #ITP #AI4Math

Palomar: a registry of Lean verified mathematics. ~Terence Tao. https://terrytao.wordpress.com/2026/08/18/palomar-a-registry-of-lean-verified-mathematics/ #LeanProver #ITP #AI4Math

A proof of the imbalance conjecture. ~ James Alexander Schreib, Yousof Yavari. https://arxiv.org/abs/2608.09191 #AI4Math #LeanProver

The shape of math to come. ~ Alex Kontorovich. https://youtu.be/ZKF6dWzOiPA #AI4Math #LeanProver

Readings shared August 17, 2026. https://jaalonso.github.io/vestigium/posts/2026/08/17-readings_shared_08-17-26/ #AI4Math #ATP #FormalVerification #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #SATsolvers

A computer-assisted proof of Sendov’s conjecture. ~ Lech Mazur. https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf #LeanProver #ITP #AI4Math

Les mathématiques du secondaire français, démontrées en Lean. ~ Michel Hua. https://lean.commutator.io/ #LeanProver #ITP #Math #AI4Math

Les mathématiques du secondaire français, démontrées en Lean. ~ Michel Hua. https://lean.commutator.io/ #LeanProver #ITP #Math #AI4Math

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. https://arxiv.org/abs/2608.10894v1 #LeanProver #ITP #AI4Math

Writing mathematics in the age of AI. ~ Main Hairer. https://proofsandprompts.com/2026/08/07/writing-mathematics-in-the-age-of-ai/ #AI4Math

The question of reasoning traces. ~ Segev Gonen Cohen. https://proofsandprompts.com/2026/08/11/the-question-of-reasoning-traces/ #AI4Math

The end of an era in mathematical research. ~ Alonso Castillo-Ramirez. https://proofsandprompts.com/2026/08/12/the-end-of-an-era-in-mathematical-research/ #AI4Math

The path to mathematical superintelligence. ~ Tudor Achim. https://youtu.be/HSxytYCWVow #AI4Math

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. https://arxiv.org/abs/2608.07396v1 #LeanProver #ITP #AI4Math

The end of mathematics. ~ Daniel Litt. https://www.daniellitt.com/blog/2026/8/11/the-end-of-mathematics #AI4Math

What sort of maths are LLMs good at? ~ Timothy Gowers. https://gowers.wordpress.com/2026/08/12/what-sort-of-maths-are-llms-good-at/ #AI4Math

Deep Vision: A formal proof of Wolstenholmes theorem in Lean 4. ~ Alexandre Linhares. https://arxiv.org/abs/2604.16507v2 #LeanProver #ITP #AI4Math

TheoremDB: A public workspace for machine mathematics. https://theoremdb.org/ #AI4Math #LeanProver