Mathematics, in progress
Each story covers the problem, the people who worked on it, what AI systems contributed, and where the Lean proof can be inspected.
Join the discussion ↗Choose a status to see what it means and which stories have it.
9 stories found
OpenAI released a proposed resolution with smooth forcing and Lean artifacts. The precise equation, assumptions, and concurrent work matter as much as the headline.
Buckmaster and Alpöge released smooth-forcing blowup results for Euler, Boussinesq, and porous media. Their work has its own history, distinct from OpenAI’s Navier–Stokes announcement.
Claude agents translated an existing proof of FLT into Lean. The advance is the scale of formal verification, with the human mathematics and its contributors still central to the story.
Anthropic reported an improvement from 41.6% to 67.2% for the proportion of zeta zeros on the critical line, with a paper and formalization. The Riemann hypothesis itself remains unproved by this work.
OpenAI released ten results with Lean certificates. The collection mixes constructions, disproofs, and improved bounds; each needs to be read on its own terms.
Alpöge announced an AI-assisted counterexample in dimension three. The surprising object led to exact checks, independent Lean work, and a search for the geometry behind it.
OpenAI announced a disproof of the expected near-linear bound for unit distances. A companion paper by external mathematicians explains the construction and its significance.
The optimal packings in dimensions 8 and 24 acquired major Lean artifacts. The community’s account explains the years of groundwork and the work still needed after an automated proof succeeds.
AlphaProof and AlphaGeometry 2 reached silver-medal standard on IMO 2024 problems. Lean provided a way to check proof attempts, while humans still translated the competition statements.