News from the edge of what is proved

Newest first. Every entry links the primary source first — the wiki, the blueprint, the abstract — and the reporting second.

1. August 17, 2026Formalization

   The 246 theorem goes through Lean's kernel

   Axiom Math published a machine-checked proof of the bounded prime gaps result that sits at the current edge of the subject, produced by its AxiomProver system and released as an interactive blueprint crediting 41 mathematicians and engineers. The proofs live in a public Lean library, PrimeGapsLib. Ken Ono, the company's founding mathematician, calls the statement "the threshold of human knowledge about prime numbers" — which is exactly the point: the interesting question is no longer whether a machine can check known mathematics, but how close to the frontier the checking can follow.

   SourcesIEEE SpectrumUnite.AI

2. June 14, 2026Formalization

   Fermat's Last Theorem: the blueprint keeps filling in

   Kevin Buzzard and Richard Taylor's blueprint for the Lean formalization was updated again. The project is not formalizing the 1995 argument but a twenty-first-century proof routed through Khare–Wintenberger and Kisin, and is funded by the EPSRC until September 2029 — a reminder that at this scale formalization is measured in years, not prompts.

   SourcesFLT repositoryBlueprint (PDF)

3. April 27, 2026Formalization

   Sphere packing is formal in dimensions 8 and 24

   The Lean project Sidharth Hariharan and Maryna Viazovska started in March 2024 reached a sorry-free main theorem in February 2026, with the last stages closed by Math, Inc.'s autoformalization model Gauss — five days for dimension 8, and dimension 24's two hundred thousand-odd lines in about two weeks. A Fields-Medal proof from 2016 is now machine-checked end to end.

   SourcesEPFLIEEE SpectrumSphere-Packing-Lean

4. November 10, 2025Formalization

   Quanta: turn proofs into checkable puzzles

   John Pavlus profiles Marijn Heule's work on SAT-based proof search: translate a statement into a tightly constrained logical problem, let a solver search, then check the resulting proof. It is a valuable counterpoint to fluent model output: a proof can be far too long to read line by line and still be mechanically checkable. The piece is an expert interview, not a benchmark of LLM capability.

   SourcesQuanta Magazine

The papers behind the headlines. Titles and author lists are reproduced as published; the line underneath says why it is on this list.

1. From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research FrontierEric Jiang, Xiao Liang, Yikai Zhang, Yingjia Wan, Mengting Li, Haikang Deng, Alexander K. Taylor, Justin Baker, Rushil Raghavan, Junyi Zhang, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei WangA UCLA-led account of what changes when language models stop solving exercises and start working where the answer is not known.arXiv:2607.07779July 10, 2026
2. Progress in Formalizing Sphere Packing in Dimension 8Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna ViazovskaThe project report behind the formalization: modular forms, the Cohn–Elkies conditions, and where an autoformalization model took over.arXiv:2604.23468April 29, 2026
3. Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative FormalizationBanri Yanahama, Akiyoshi SannaiNames the failure the kernel cannot catch: a proof that type-checks while the statement says something other than what was meant.arXiv:2604.16347 · AIPV 2026April 23, 2026
4. Olympiad-level formal mathematical reasoning with reinforcement learningThomas Hubert, Rishi Mehta, Laurent Sartran et al.The AlphaProof paper shows why formal grounding matters: Lean checks the resulting proof term step by step. Its silver-medal-equivalent 2024 IMO result required multi-day computation and does not establish autonomous research-level mathematics in general.Nature 651, 607–613 (2026)November 12, 2025