Getting the (In)Formal Statement Right

It's clear to everyone now that LLMs have changed how mathematics gets done, and other fields are close behind. OpenAI's model proved finite-time blowup for the Navier–Stokes equations with a smooth, compactly supported force, and as Quanta reported, another model formalized the proof in Lean 17 hours later. Anthropic's model wrote about 13 million lines of Lean for Fermat's Last Theorem in 11 days. LLM agents have verified an operating-system kernel, production cryptography, a compiler and Ethereum bytecode.

What excites me most about all of this is that we're getting closer to a world where much more of mathematics can be formalized, checked, and built upon. I find the progress remarkable. We can now generate proofs at a scale that would have been difficult to imagine even a few years ago, what Mistral calls proof abundance, and Lean gives us a way to verify those proofs without having to read every line. Kim Morrison pointed out back in 2024 that autoformalization is on the critical path, and I think the recent progress, along with the case for formalizing all of mathematics, has made that increasingly clear.

But there's a problem that I think deserves much more attention. How do we know that the statement being proved is actually the statement we intended to formalize? A proof can be completely correct in Lean while establishing something weaker, different, or even unrelated to the original mathematical claim. And when we translate that formal result back into natural language, it's surprisingly easy to lose the distinction again. For me, this is one of the most important challenges in autoformalization today. I want us to get to a point where we can trust not only the proof, but also the mathematical meaning of what has been formalized. That's two goals: correctness, knowing that a result is true and which result it is, and understanding, a person being able to read the statement, see what was proved and why, and use it.

Here is a small example I found in openai/math, the release where a model wrote hundreds of research papers and put a Lean challenge next to each headline. One paper is about Yau's conjecture on nodal sets. The nodal set of a Laplace eigenfunction is its zero set, and Yau conjectured that on a closed n-dimensional manifold, the (n−1)-dimensional measure of the nodal set of an eigenfunction with eigenvalue λ stays between two constant multiples of √λ. The paper works on S4 × S1, where that measure is the Hausdorff measure H4, and it constructs a smooth metric there whose eigenfunctions beat the upper bound by a fixed power: H4/λ1/2+ε0 → ∞ for some ε0 > 0. And the release ships a Lean proof of its challenge.

The challenge asks for less: it requires only H4/√λ → ∞, so any violation of the bound counts. I like to see a gap like this on a concrete sequence, and √λ log λ does the job. It beats √λ by a factor of log λ that keeps growing, so it meets the challenge, but it falls behind λ1/2+ε0 for every fixed ε0 > 0, so it misses the paper's claim. The sequence is abstract and says nothing about real eigenfunctions: all it shows is that the two conditions differ. Here is the difference, with the nodal measures replaced by that sequence:

-- The Lean challenge asks for this, with h the nodal measures: def LeanShape (h : ℕ → ℝ≥0∞) (lam : ℕ → ℝ) : Prop := Tendsto (fun k ↦ h k / ENNReal.ofReal (Real.sqrt (lam k))) atTop (𝓝 ⊤)

-- The paper's Theorem 1.1 claims this, a fixed power ε₀ more: def PaperShape (h : ℕ → ℝ≥0∞) (lam : ℕ → ℝ) : Prop := ∃ ε₀ > 0, Tendsto (fun k ↦ h k / ENNReal.ofReal (lam k ^ ((1 : ℝ) / 2 + ε₀))) atTop (𝓝 ⊤)

-- A sequence that separates them: λ_k = k + 1, h_k = √λ_k · log λ_k. def sibLam (k : ℕ) : ℝ := (k : ℝ) + 1

def sibH (k : ℕ) : ℝ≥0∞ := ENNReal.ofReal (Real.sqrt (sibLam k) * Real.log (sibLam k))

-- The challenge's condition holds for it... theorem leanShape_sib : LeanShape sibH sibLam := by -- (eight lines: the ratio is log λ_k, which goes to infinity)

-- ...and the paper's fails, for every ε₀ > 0. theorem not_paperShape_sib : ¬ PaperShape sibH sibLam := by -- (fifteen lines: log λ_k / λ_k^ε₀ tends to 0)

#print axioms OAI.Yau.Target.not_paperShape_sib -- 'OAI.Yau.Target.not_paperShape_sib' depends on axioms: [propext, Classical.choice, Quot.sound]

What I found interesting here wasn't a mistake in the proof. The proof establishes exactly what the Lean statement asks for.1 The issue is that the Lean challenge and the theorem in the paper make different mathematical claims. This is precisely why I think semantic fidelity matters so much in autoformalization. We can have a perfectly valid proof, checked by Lean, and still end up communicating a result that hasn't been formally established. As more of these results are generated automatically, I think we need to become much more careful about this distinction.

I've also been following many of the autoformalization discussions on Lean Zulip, and one thing I've appreciated about the community is how seriously people take the distinction between a checked proof and a faithful mathematical statement. The discussions around Meta's Atlas are a particularly interesting example. Atlas was reported as more than 45,000 declarations formalized from 26 textbooks. Formalizing tens of thousands of declarations is an impressive achievement, but it also raises a much harder question: how do we know that those declarations faithfully represent the original mathematics? This is not something we can settle by counting successful Lean compilations. One reader wrote of a book listed as 56 percent formalized that "the reality is that 0% of the statements here are accurately formalized", a post later quoted by Bastounis, Circelli and Hansen, and the complaint was about the statements, not the proofs: most of them had been checked only by other models.

When an AI system says it has formally proved a result, I want to know what to check before trusting it, and I keep the jobs apart. The proof has to prove the statement, the statement has to mean what the source meant, and the natural-language version has to say what the statement says. Lean does the first one. Today the other two are mostly done by people, though I expect agents to take on more and more of them. As they do, I think the human job changes from checking each statement to deciding what's worth formalizing, which definitions are the right ones, and what a result means. For understanding there are two more questions: whether the decomposition keeps the structure of the argument instead of giving one opaque certificate, and whether the abstractions are meaningful, general enough and compatible with the rest of mathematics. A successful kernel check answers only the first.

Over time, and especially from reading the community discussions and looking through generated formalizations myself, I've started using a few checks that I find particularly helpful. Most of these ideas come from people in the Lean community, and I think they're worth making more systematic as autoformalization becomes more common. Here are six things I look for when evaluating a formal result. Today I run most of them myself, with agents helping. As models get better at these semantic questions, I expect agents to run more of them, and I'd like the list to work as a specification for those agents as much as a habit for people.

Proofs can come from anyone because of how Lean is built: a proof is a term, its statement is the term's type, and the kernel checks the one against the other and never asks where the term came from. Once we've fixed the statement and its definitions, a proof from a graduate student, a language model or an alien gets the same treatment. Lean builds this in: any two proofs of the same proposition are equal by definition, so example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl goes through. Jason Rute has made the same point on Zulip: once the statement is separated from the proof, the "referee" only needs to check "the statement and definitions used in the statement".

I rely on Comparator to turn this into a protocol, and since Lean 4.35 it ships with Lake as lake comparator. I write a challenge file that states each theorem with sorry and name the axioms I allow. Comparator builds the untrusted solution in a sandbox and checks that each theorem has my statement, down to every constant it mentions, uses only those axioms, and is accepted by the kernel. With --paranoid it also replays everything through five more checkers, among them con-leche, whose verified mode is proved in Lean never to accept a theorem of False.

Lean's own manual calls this the gold standard for "un-reviewed AI-generated proofs and programs", and it says what it leaves to the reader, ending with "no human error or misleading presentation of the theorem statement in the trusted challenge file". No checker covers that condition, so it falls to a person, and to me that's where most of our attention should go.

One thing Comparator can't check for us is an open definition, one the challenge leaves as sorry for the solver to fill in. The Comparator docs give the example themselves: if the challenge is RiemannHypothesis ↔ ChallengeSolution with def ChallengeSolution : Prop := sorry, then def ChallengeSolution : Prop := RiemannHypothesis solves it by reflexivity. So when a challenge leaves a definition open, I read what the solver filled in myself.

The same rule, that a reader checks the statement and its definitions but never the proof, tells us what to read when theorem A depends on theorem B. If A's proof uses a proved B, the kernel checked B, so nobody needs to read it, however many million lines it took; if B is an axiom or rests on a sorry, the axiom check rejects it. If A takes B as a hypothesis, A is a conditional theorem and its headline has to say "assuming B". And if A's statement mentions B's definitions, those definitions are part of the statement and somebody has to read them. Axiom's CFSG is this third kind: it says every finite simple group is isomorphic to a group in Tau Ceti's list, so reading it means reading how the groups in that list are defined.

Lean has two engines, one that checks proofs and one that compiles programs. On the checking side, the elaborator runs our tactics and automation, and none of that is trusted: it only proposes declarations. The kernel checks each one, a replay checks them all again, and every axiom is listed. The kernel is small, and small isn't perfect: Mario Carneiro said on Zulip that "there are bugs in it like any other software, but it is held to a high standard", and Jason Rute added that the independent checkers only reassure us if we run them.

The compiler is the other engine. It turns definitions into C that runs on Lean's runtime, and the kernel never sees any of it. Compilers and the runtime deserve a post of their own, and I'm writing one soon. Here one tactic matters.

native_decide is the bridge between the two: it compiles a decision procedure, runs it, and since Lean 4.29 adds a fresh axiom saying the answer came back true. A proof that uses it trusts the compiler, and one mismatched @[implemented_by] is enough to prove False. This compiles on Lean 4.35 without Mathlib:

-- Compiled code runs fast wherever slow is called; the kernel sees slow. def fast (_ : Nat) : Bool := false @[implemented_by fast] def slow (_ : Nat) : Bool := true

theorem slow_true : slow 0 = true := rfl theorem slow_false : slow 0 = false := by native_decide -- runs fast theorem oops : False := Bool.noConfusion (slow_true.symm.trans slow_false)

#print axioms oops -- 'oops' depends on axioms: [slow_false._native.native_decide.ax_1_1]

I take three habits from this.

I think writing the right formal statement is often much harde