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.
OpenAI's openai/math repository holds manuscripts and proof artifacts produced by an internal OpenAI model, organized into 372 families, with 300 of 719 top-line results formalized in Lean. An October 7, 2026 update withdrew three manuscripts after a sign error and revised 14 others.
Checked against: openai/math
A repository by @dpwoodru contains a complete, machine-checked Lean 4 proof of the general Courtade–Kumar inequality (the most informative Boolean function conjecture), formalizing the paper by Z. Chen, A. Gohari, A. Javanmard, H. Lin, V. Mirrokni, C. Nair and D. P. Woodruff. The whole proof spans 45,500 modules.
Checked against: dpwoodru/general-courtade-kumar-lean
Google's launch post for Gemini 4 Argon (dated 2026-10-13) reports an arcsin implementation, a building block in recent quantum simulation algorithms, written by Argon and formally verified in Lean. It cuts spacetime cost by more than 100x compared to a published quantum CORDIC baseline.
Checked against: blog.google
A paper in Science by George Tsoukalas, Swarat Chaudhuri and coauthors describes an agent for formal proof search that autonomously resolved nine of 353 open Erdős problems and proved 44 of 492 On-Line Encyclopedia of Integer Sequences conjectures. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes.
Checked against: science.org
Scott Armstrong writes that autoformalization of research-level mathematics has become easy, citing a Lean formalization of a 145-page paper with Vicol in about 36 hours (270k lines of code), and makes the agent skill files public. A separate Xena post weighs mathematicians' reactions to AI, noting "You cannot fool Lean."
Checked against: scottnarmstrong.comxenaproject.wordpress.com
Ziyang Qin, Yuan Liao, Ayush Khaitan, and Bennett Chow formalize the smooth three-dimensional Poincaré conjecture via Ricci flow with surgery and finite-time extinction. Together with the Moise smoothing theorem, the result yields the topological three-dimensional Poincaré conjecture.
Checked against: arXiv:2609.33842
Geby Jaff of Vals AI had 10 Claude Opus 5.5 agents coordinate on a message board; after about 15 hours and 733 messages they proposed C-HD, whose Lean proof (checked with the Lean Comparator tool) establishes a strict asymptotic improvement over n log n for a stated density of edges. The constants are enormous, so no practical speedup is established.
Checked against: vals.ai
OpenAI said 10,000 autonomous AI agents found a singularity in the Navier-Stokes equations in three dimensions, with the result formally checked in Lean. Hours earlier, Tristan Buckmaster at New York University and Levent Alpöge at Anthropic reported Lean-verified proofs for three related results, including one for the Euler equations.
Checked against: quantamagazine.orgblog.computationalcomplexity.org
Working largely autonomously over 11 days, Claude wrote 13 million lines of Lean (over 5x the size of Mathlib, the principal community library) and proved 29,500 intermediate theorems. Kevin Buzzard compiled the code and ran comparator on it, and the full proof is on GitHub with a written walk-through.
Checked against: anthropic.comxenaproject.wordpress.comanthropics/fermats-last-theoremnature.com
Yinjie Li presents an independently obtained, structurally different proof of the strict even-dimensional case of the Harwit and Sloane conjecture, formalized in Lean 4 conditional on Frankel and Urschel's Lemma 2.1 as an explicit external input. Finite evaluations use Lean's native evaluator, with their trust boundary documented.
Checked against: arXiv:2608.29750
Shuze Chen, Kunal Marwaha, Xiaoyang Lu, Henry Yuen and Tianyi Peng introduce Prove2Me, where users launch formalization "missions" and AI agents contribute Lean proofs toward completion, building on and reusing one another's results. One listed mission targets Mathlib's open conway_99 problem on a strongly regular graph with parameters (99,14,1,2).
Checked against: arXiv:2608.28433prove2.me
Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková and Christoph Thiele released a blueprint and Lean 4 formalization of a quantitative strengthening of Tao's norm-convergence theorem, answering an open question of Avigad and Rute. The proof was autoformalized during a one-week period using coding agents under human supervision, producing roughly 107k lines of code.
Checked against: roos-j/lean-nctarXiv:2608.27321
The Vilin97/MazurTheorem repository targets the classification of rational torsion on elliptic curves, using Mazur's degree-one formal-immersion argument at the auxiliary prime 5. The project reports an integrated score of 17.2% on its 48-node, 1,000-point theorem DAG, and it accepts claims only on contracts marked open or research_open.
Checked against: Vilin97/MazurTheorem
Jiaxin Yuan and coauthors introduce MathAdv, a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics, finding formalization remains a major bottleneck. Separately, Wenqian Ye and coauthors present ProofEvolve, where the Lean kernel verifies every proof transition. It achieves the highest average solve rate among the evaluated proof systems on three competition-level Lean benchmarks.
Checked against: arXiv:2608.25449arXiv:2608.26334
Scott Armstrong wrote on X that in March, Lean formalization was not possible for his papers, and by August it had become essential and increased the efficiency of his workflow dramatically. Scott Armstrong says the papers are getting written informally and finished much faster because of the Lean formalization.
Checked against: @scottnarmstrong on X
Palomar, an initiative incubated by the Lean FRO and by ICARM, registers GitHub repository snapshots after checking with the Lean tool Comparator that proofs match the claimed statements, and with a large language model that the informal description matches. Terence Tao stresses that Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.com
Palomar, a public, searchable registry of machine-checked Lean formalizations incubated by the Lean FRO and ICARM, is now open for submissions, Terence Tao announced. Submitted repository snapshots are checked mechanically with the Lean tool Comparator and by a large language model, though Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.comLinkedIn post
Researchers including Kaiyu Yang, Soonho Kong, Jingxuan He, and Dawn Song introduce Vero, a benchmark of 43 multi-module instances sourced from real-world repositories, each a multi-module Lean 4 repository with predetermined API interfaces. The strongest agent fully solves only 27 of 43 instances.
Checked against: arXiv:2608.13522
An unreleased research version of Claude increased the lower bound for the fraction of Riemann zeta zeros satisfying the Riemann hypothesis from 41.6% to 67.2%. Claude and Eric Easley produced a Lean formalization that passes comparator, the validation tool originally developed by Lean FRO with feedback from the AIMO team.
Checked against: anthropic.comanthropics/zeta-23-leanleanprover/comparator
Arnav Mehta of Pramaana Labs reports that the company's system, which translates each question from English into Lean and then proves it, solved all 6 IMO 2026 problems in under 7 hours for less than $150. Pramaana Labs earlier announced $27 million in seed funding led by Khosla Ventures.
Checked against: lnkd.intechcrunch.com
LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean, that generates a program, its formal specification, and a machine-checkable proof from a natural-language description. The paper, accepted to ASE'26, reports that property-based testing validates specifications before any code is synthesised.
Checked against: arXiv:2604.16584lnkd.in
CSLib, the Lean Computer Science Library, now includes a proof of the FLP (Fischer, Lynch and Paterson) result: consensus is impossible in a distributed system with a faulty process and asynchronous messaging. Ching-Tsun Chou formalised the constructive pen and paper proof by Hagen Völzer from 2004.
Checked against: lnkd.inleanprover/cslib
Alex Kontorovich announced the release of Tau Ceti, which Alex Kontorovich describes as the brainchild of Kim Morrison at the Lean FRO and a "Mathlib for AIs". The stated aim is to move fast and get a whole lot more formalized math than can be done at the scale of human review.
Checked against: @AlexKontorovich on X
Mistral AI's documentation lists Leanstral 1.5, dated June 30, 2026, as an updated Lean 4 formal proof engineering model optimised for automated theorem proving and autoformalization. The Apache 2.0 model has 119B total parameters (6.5B active) and a 256k context, though the page marks it deprecated with a deprecation date of 9/29/2026.
Checked against: docs.mistral.ai