What does it mean to formalize a proof? Can we really trust a formalized proof, even if written by an LLM?

A summer of breakthroughs

This summer, LLMs helped write remarkable proofs of long-standing open problems.

Two examples among many:

• A complex structure on S^6

• The Navier–Stokes problem

OpenAI announcement · 8 September 2026

What is formalization?

Formalization means writing mathematical statements and proofs in a precise language so that a computer can check every step of the proof.

• Every step needs justification, including “obvious” ones. Automation can fill in many of the details.

• As we need to justify everything, this process can be very tedious.

• Proof assistants help us write these proofs, with mathematical notation and immediate feedback.

• Making definitions and assumptions explicit often deepens our understanding of the mathematics.

Lean and mathlib

• Lean is an open-source proof assistant and functional programming language. We use it to write mathematical statements and proofs that Lean checks.

• mathlib is a community-maintained library of mathematical definitions and theorems, together with their proofs.

• It covers many areas of mathematics, from linear algebra and analysis to smooth manifolds and schemes.

• Libraries like mathlib let results from different areas work together: we can reuse existing theorems instead of proving everything from scratch.

An example: the Heine-Cantor theorem

Theorem. Let X and Y be metric spaces, with X compact. Every continuous map f : X \to Y is uniformly continuous.

Proof sketch. Fix \varepsilon > 0 and consider

K_\varepsilon = \{(x,y) \in X \times X \mid d_Y(f(x),f(y)) \ge \varepsilon\}.

• Compactness. By continuity, K_\varepsilon is closed in compact X \times X, hence compact.

• A positive minimum. Choose (p,q) \in K_\varepsilon minimizing d_X(p,q) and set \delta = d_X(p,q). Then \delta > 0, since p=q would give \varepsilon \le d_Y(f(p),f(q)) = 0.

• Uniform continuity. If d_X(x,y)<\delta, minimality gives (x,y)\notin K_\varepsilon, so d_Y(f(x),f(y))<\varepsilon. \square

mathlib supplies the definitions and compactness results used here, and already contains the Heine–Cantor theorem itself.

Can we really trust a Lean proof?

Can we trust a human-written and human reviewed proof?

Can we trust a human-written and human reviewed proof?

Can we trust a human-written and human reviewed proof?

Retracted in 2023

Can we trust a human-written and human reviewed proof?

How does Lean check a proof?

• Correctness is checked by Lean's kernel, a small trusted component.

• Independent external checkers can verify Lean proofs as well.

• Lean's standard axiomatic system is equivalent in consistency strength to ZFC plus universes.

• For each theorem, we can inspect its axiom dependencies and ask an external checker to verify its proof.

• We still need to check that the formal statement expresses the mathematics we intend.

To what extent can we trust a human-written Lean proof?

• In July a claimed disproof of the Collatz conjecture compiled. It was not a disproof: it exploited a bug in the kernel, and proved False with only the standard axioms.

• Over the following weeks four more bugs were found in the kernel. All of them are fixed, in Lean v4.33.1.

• Every one of them was reached through heavy, deliberate metaprogramming. Nothing of the kind happens when you are simply writing mathematics.

• So it remains extremely unlikely that a mistake in a human-written proof gets past Lean. That is not what you should worry about.

To what extent can we trust an LLM-written Lean proof?

• With LLM-written code, the trust problem is harder: we must treat the LLM as an adversary.

• The code can be enormous and difficult to digest: Claude's formalization of Fermat's Last Theorem contains 13 million lines of Lean.

• Tools such as Comparator check that the LLM has not “cheated”.

• Independent proof checkers and up-to-date Lean versions provide further protection against exploits, including previously unknown kernel bugs.

• Expert review is still needed: all the results announced this summer have undergone such a review.

What LLM-written Lean cannot do

Help us understand the proof

Check the meaning of definitions and statements

Checking statements and definitions

• Lean cannot guarantee that a definition or statement expresses what we have in mind.

• Reading Lean code is not always easy.

• We can trust mathlib, which has undergone extensive and careful human review. For example, we can rely on its definition of \mathbb{R}: mathlib proves that it is a complete ordered field.

• The definitions involved have themselves been carefully reviewed by humans.

• A concise statement using mathlib's standard definitions lets us check directly that the theorem says exactly what we intend.

The Formal Conjectures repository

• Formal Conjectures collects statements of mathematical problems in Lean, using mathlib, including many open conjectures.

• Contributions undergo careful review of both definitions and statements.

• When autoformalizing a proof of a conjecture in the repository, we can reuse its formal statement.

• This approach was used for the complex structure on S^6 and the Navier–Stokes problem.

• Work is underway on a formal statement of the Hodge conjecture.