AI Theorem Proving in Lean 4: Where It Stands in 2026

Recommendation: In competition mathematics, AI provers now produce kernel-checked Lean 4 proofs for every PutnamBench problem, so that benchmark no longer separates the leading systems. In research mathematics, the practical gain is in routine lemmas, Mathlib search, and proof repair, while deciding what the formal statement should say stays with the mathematician.

Lean 4 and Mathlib in numbers

Lean 4 is a programming language and proof assistant. A proof in Lean is code, and a small trusted kernel checks every step. If the file compiles with no sorry (Lean's placeholder for a missing proof), the theorem as stated is proved.

Most of the mathematics lives in Mathlib, the community library. On 16 October 2026 its statistics page reported:

That size matters for AI. A prover that can search Mathlib does not need to rebuild real analysis or group theory from axioms, and the gaps in Mathlib are where both humans and machines slow down.

Results from AI provers, with sources

The results below come from papers and the official benchmark leaderboard. "Vendor-reported" means the team that built the system ran the evaluation.

The PutnamBench paper (Tsoukalas, Lee, Jennings et al., NeurIPS 2024 Datasets and Benchmarks) introduced the benchmark as a hard open challenge, built from Putnam competition problems formalized by hand. In July 2024 the best Lean entry on its leaderboard solved one problem.

The chart reads the official results file of the leaderboard, which changes often. Each bar is a new record entry with its date and system, and the bar length is the number of problems solved; the benchmark has 672 Lean problems today, and earlier versions had 640 to 660. Four systems now report 672 of 672: Aleph Prover (Logical Intelligence), Humanfia, NEAR AI and Forall (Astrio). The NEAR AI entry is the one with fully open data. Its verifier rejects sorry, new axioms and native_decide (a tactic that trusts compiled code instead of the kernel), checks that the theorem statement is unchanged, and prints the axioms each proof uses.

Beyond competitions

Competition problems have known answers and short proofs. Open problems do not. In January 2026, Nat Sothanaphan published a write-up of Erdős Problem #728. The proof was produced by GPT-5.2 Pro together with Harmonic's Aristotle, run by Kevin Barreto, and the result is a Lean proof. The write-up describes it as the first Erdős problem regarded as fully resolved autonomously by an AI system. The human contribution was turning the Lean proof back into readable mathematics.

What the results mean for working mathematicians

Checking is cheap, stating is not. The kernel reports whether a proof proves the statement in the file. It cannot report whether that statement is the theorem the author meant. The NEAR AI run found two PutnamBench problems with defective formalizations and solved corrected versions instead. Those formalizations were written and reviewed by experts for a published benchmark, so the same failure can occur in any project.

Saturated benchmarks stop measuring progress. When four systems reach 672 of 672, PutnamBench no longer separates them. Cost is now the variable: the leaderboard lists averages from $0.17 to $74 per problem across those four entries. Harder sets such as Fate-X, where Seed-Prover 1.5 reports 33%, say more about research-level ability.

Most results are vendor-reported. AlphaProof, Seed-Prover and Aristotle are closed systems. Their Lean output can be checked, which is the point of formal proof, but the full pipeline and compute budget usually cannot be reproduced from outside.

The useful work today is routine lemmas. In a Lean project, a coding agent is good at closing small goals, finding the Mathlib lemma the mathematician half remembers, and repairing proofs after a Mathlib update. The mathematician still chooses definitions, splits the argument into lemmas, and reads every statement the agent writes.

A learning path into Lean 4

1. The basics, in the browser. The Natural Number Game is an interactive tutorial: the player proves properties of addition and multiplication on the natural numbers, one level at a time. The Lean web editor runs short examples against the latest Mathlib, and its README says larger projects are out of scope.
2. Mathematics in Lean. The standard book for mathematicians works through sets, functions, number theory, algebra and analysis using Mathlib. The community learning page lists alternatives.
3. Searching Mathlib. Loogle finds lemmas by constant, name fragment, subexpression or conclusion pattern. LeanSearch takes plain-language queries (Gao, Ju, Jiang, Qin and Dong, arXiv:2403.13310, 2024). Most early friction is not knowing a lemma's name.
4. The Zulip chat. The Lean Zulip chat is where Mathlib maintainers and newcomers talk. Questions with a minimal working example get fast answers.
5. Something small and already known. A lemma from the learner's own paper or lecture notes teaches more than a famous theorem. The statement comes first, and a colleague reads it before the proof starts.
6. An AI agent, last. Once the learner can read Lean, an agent saves time. Before that, there is no way to tell whether it proved what was asked.

Lean 4 and an agent in one Codespace

A local Lean setup needs elan, lake, a Mathlib dependency and a multi-gigabyte cache. The earlier post on Lean 4 and Mathlib in cloud VS Code walks through that setup and the alternative.

In Oyren, Lean 4 + Mathlib is an add-on in the Codespace launch wizard. It starts a cloud machine with VS Code in the browser, the Lean toolchain, the Mathlib cache and the infoview. Coding agents run in the same Codespace, so an agent can propose a tactic while the mathematician watches the goal state. Notes, with LaTeX equations, and the source PDF stay in the same workspace.

The capture is step 1 of 5 of the launch wizard. The selected Codespaces card is the cloud machine, and the Add-ons panel holds the Lean 4 + Mathlib checkbox, which installs the Lean 4 toolchain with the Mathlib cache and the editor's infoview. The optional First prompt field below it opens the Codespace in Chat with the agent already working; left empty, the Codespace opens in the editor. The add-on does not check proofs inside notes, and an agent's output still needs the reading described above. The Lean 4 and LaTeX maths notes page shows how the notes and the Codespace fit together. A Codespace with the Lean 4 + Mathlib add-on launches from any workspace.