Weekly
News about Lean, the theorem prover and programming language.
AI systems that prove or formalize mathematics, large formalizations, and benchmarks. 35 items, newest first.
Formal Frontier is a new project focused on responsible, scalable, and open-source AI-driven autoformalization of mathematics, with XTX Markets supporting it. Its initial phase covers a community autoformalization specification, open-source tooling, and autoformalized texts chosen to fill gaps in Mathlib's existing coverage.
Checked against: mathlib-initiative.org
The paper describes how Maryna Viazovska's 2016 solution of the sphere packing problem in dimension 8 was formally verified in Lean in February 2026, with the final stages done by Math, Inc.'s autoformalization model Gauss. It discusses the techniques used, the collaboration between humans and Gauss, and remaining project objectives.
Checked against: arXiv:2604.23468
Alex Meiburg asked Aristotle to formalize a Z80 emulator, build an assembler, and write a BigNum GCD in about 80 assembly instructions, then verify it by modeling the whole CPU execution. After 14 rounds of submitting to Aristotle (without editing the prompt), the proof succeeded.
Checked against: leanprover.zulipchat.com
Kyuhee Kim, Auguste Poiroux and Antoine Bosselut evaluate GPT-5 and DeepSeek-R1 on 303 first-order logic problems: GPT-5 fabricates axioms during proof generation, while DeepSeek-R1 mistranslates premises. Other papers introduce PRIME, a benchmark of 156 theorems annotated in Lean 4, analyze tool-augmented formalization agents, and formalize the Wu-Ritt characteristic set method.
Checked against: arXiv:2604.19459arXiv:2604.19000arXiv:2604.16538arXiv:2604.14912arXiv:2604.18882
Mistral AI released Leanstral, with 6B active parameters and weights under an Apache 2.0 license. On FLTEval, a new suite built from pull requests to the FLT project, Leanstral pass@2 scores 26.3, beating Sonnet by 2.6 points while costing $36 to run versus Sonnet's $549.
Checked against: mistral.ai
Formalizing a 2006 paper on the stability of the two Higgs doublet model (2HDM) potential, using Mathlib and Physlib, revealed an error invalidating its main theorem. The paper calls this, to the best of its knowledge, the first non-trivial error in a physics paper found through formalization.
Checked against: arXiv:2603.08139
Math, Inc. used Gauss to help formally verify Maryna Viazovska's Fields Medal-winning sphere packing results, proving all remaining 8-dimensional results in 5 days and autoformalizing the 24-dimensional case in two weeks. The formalization grew from 70k to about 200k lines.
Checked against: math.inc
Gauss, a Math, Inc. reasoning agent built to formalize proofs automatically, produced over 200,000 lines of Lean code for Maryna Viazovska's 24-dimensional proof in two weeks, without a preexisting blueprint. The work follows the 8-dimensional formalization announced on February 23, which built on the Formalising Sphere Packing in Lean project.
Checked against: spectrum.ieee.org
Yann Fleureau announced Numina-Lean-Agent, an open-source agentic framework for autoformalization and theorem proving using generic AI models. The announcement reports 12/12 on Putnam 2025 and a formalization of the "Effective Brascamp-Lieb inequalities" research paper, more than 90% of it AI-generated.
Checked against: LinkedIn post
AxiomProver, an autonomous AI theorem prover built by Axiom, solved 12 out of 12 problems from the Putnam Competition, 8 of them within the strict exam time limit, producing formal proofs in Lean. One combinatorial step in Problem A5 required 2,054 lines of formal proof.
Checked against: LinkedIn post
A Hacker News thread on the claim that Erdos problem #728 "was solved more or less autonomously by AI" drew 619 points and 363 comments. A Harmonic employee said Aristotle, the company's system, can translate an informal English proof into Lean, and commenters debated how to check that a theorem statement is formalized correctly.
Checked against: news.ycombinator.com