Getting the (In)formal Statement Right

Robert Joseph George · November 2026

Here's a result from 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 zero sets of Laplace eigenfunctions, whose size Yau conjectured grows like √λ. The paper constructs eigenfunctions that beat the upper bound by a fixed power, with H⁴/λ^1/2+ε₀ → ∞ for some ε₀ > 0, and the release ships a Lean proof of its challenge.

The challenge asks for less. It only requires H⁴/√λ → ∞, any violation of the bound at all. Here are the two growth conditions side by side, with the nodal measures replaced by an arbitrary sequence, and a sequence that satisfies the challenge's condition and not the paper's:

The paper's claim and the Lean challenge, as growth conditions

-- 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]

Nothing is wrong with the proof. The statement is just weaker than the paper's theorem, and checking the proof would never have told you, because the proof proves exactly what the statement says.¹

Statements like this matter more every month, because machines now write a lot of the proofs. OpenAI's model proved finite-time blowup for the Navier–Stokes equations with a smooth, compactly supported force, and another model formalized the proof in Lean seventeen hours later. Anthropic's model wrote about thirteen million lines of Lean for Fermat's Last Theorem in eleven days. Agents have verified an operating-system kernel, production cryptography, a compiler and Ethereum bytecode. Mathematics is heading toward what Mistral calls proof abundance, and I'm really excited about it. Once a piece of mathematics is formal it's unlocked: you can search it, reuse it, hand it to the next agent and build on it without rereading anyone's proof. The more of it is formal, the faster the next discovery comes. Kim Morrison said on Zulip back in 2024 that autoformalization "is on the critical path", and the recent case for formalizing all of mathematics argues that a coordinated effort "could enormously expand mathematical exploration and discovery".

For me formalization has two goals, correctness and understanding. Correctness means knowing that a result is true and exactly which result it is. Understanding means a person can read the statement, see what was proved and why, and use it. A checked proof gives you only the first half of correctness. Everything else goes through the statement and the English we write about it, and that's where things go wrong. I spend a lot of time in the autoformalization threads on the Lean Zulip, and one story keeps repeating: somebody announces a big formal library, somebody else opens the files, and the statements say something else. When Atlas was reported as more than 45,000 declarations formalized from 26 textbooks, 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. Every proof had been checked. The statements had mostly been checked by other models.

It helps me to keep three jobs apart. The proof has to prove the statement, the statement has to mean what the source meant, and the English has to say what the statement says. Lean only does the first one.

A doodle: a paper on the left, the Lean statement in the middle, a headline speech bubble on the right, and a stack of proof pages below the statement. The arrows from the paper and to the headline are dashed and labelled "people check"; the arrow from the proof is green and labelled "Lean checks". — Three jobs, and only one of them is done by a machine.

Before you call a Lean result done

Here's the short version, the five things I check before I call a result done. The rest of the post is why.

Freeze the statement first, then run Comparator. Before any proving, put the theorem, with sorry as its proof, and every definition it uses in a challenge file, and leave no definition open. Pin Lean and Mathlib, and at the end check the proof against it with lake comparator. That's for mathematics; code needs more.
No extra axioms. Only propext, Classical.choice and Quot.sound, as a replay of the proof lists them: no sorry, no axiom, no native_decide. If you need an assumption, make it a hypothesis.
Have an agent read the statement, then a person. Give both the elaborated statement, its definitions and the exact source, but not the proof, and write down every place the Lean differs from the source.
Try to break it. Make sure the hypotheses aren't contradictory by accident, and test every new definition on examples you already understand.
Write the English from the Lean. The headline says what the statement says, and the gaps are listed next to it.

Why the proof can come from anyone

A Lean proof is a term, and its statement is the term's type. The kernel checks one against the other and never asks where the term came from. Once the statement and its definitions are fixed, a proof from a graduate student, a language model or, if one ever opens a pull request, an alien gets exactly the same treatment. Lean even 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 put it nicely on Zulip. Once the statement is separated from the proof, the "referee" only needs to check "the statement and definitions used in the statement".

Comparator turns that into a protocol, and since Lean 4.35 it ships with Lake as lake comparator. You write a challenge file that states each theorem with sorry, plus a configuration naming the theorems and the axioms you allow. Comparator builds the untrusted solution in a sandbox and checks three things: each theorem has exactly your statement, down to every constant it mentions; it uses only the allowed axioms; and the kernel accepts it. With --paranoid it also replays everything through five more checkers.²

A doodle: the challenge box on the left, read by a stick figure; Comparator in the middle with three ticks for same statement, only those axioms and kernel accepts; on the right, a student, a robot and an alien inside a dashed box labelled anyone, never read, with a stack of proof pages. — People read the challenge. Anyone can send the proof.

The Lean manual calls this the gold standard for "un-reviewed AI-generated proofs and programs", and it's honest about what's left, ending with "no human error or misleading presentation of the theorem statement in the trusted challenge file". Most of this post is about that last line.

One thing Comparator can't check for you is an open definition. It compares those only by name, type, universe levels and safety, so def ChallengeSolution : Prop := RiemannHypothesis "solves" a challenge that asks for a Prop, and the Comparator docs say so themselves. If a challenge leaves a definition open, read it yourself.

What Lean actually trusts

Lean has two engines in it, and it matters which one a proof goes through. The elaborator runs your tactics and automation, whoever wrote them, and none of it is trusted: it only proposes declarations for the kernel to check, and any axiom it adds is listed. The kernel is the trusted part. It's small, but trusted doesn't mean perfect. As Mario Carneiro put it on Zulip, "there are bugs in it like any other software, but it is held to a high standard". When one is fixed, rechecking on the new toolchain shows whether any proof depended on it, and Jason Rute added that the independent checkers only reassure you if you actually run them.

The compiler is the other engine. It turns definitions into C so programs run fast, swaps in any @[implemented_by] or @[extern] replacement, and nothing it produces is checked by the kernel.

A doodle with two lanes. Top: tactics and automation feed a proof term to the kernel, which accepts it and lists its axioms. Bottom: the compiler produces running code that the kernel never checks. A dashed orange arrow labelled native_decide, trust me, it's true, goes from the running code up into the kernel and enters as an axiom. — The kernel checks terms. Compiled code is never checked, and native_decide carries its answer across.

native_decide connects the two. It compiles and runs a decision procedure and, since Lean 4.29, adds a fresh axiom saying the answer was true, so the proof now trusts the compiler and every replacement on the way. A mismatched @[implemented_by] is enough to prove False. This compiles on Lean 4.35 without Mathlib:

native_decide proving False

-- 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]

Three habits come out of this.

Do computations in the kernel. decide, decide +kernel, rfl and norm_num leave a term the kernel checks and add no axiom of their own. For a big search, find the answer outside Lean and check a certificate inside it. native_decide is fine while you're exploring, but I wouldn't ship it.
Read the axioms off a replay, not the source. lake check and Comparator replay the exported proof and list what it depends on. The source can mislead: a bad declaration added under debug.skipKernelTC can report no axioms at all, and agents have spelled the keyword "ax" ++ "iom" to get past text filters.
Keep assumptions as hypotheses. Shreyas Srinivas made the case on Zulip. An axiom is not part of any theorem's statement, so you only see it by asking for a theorem's dependencies, and even a private one carries into every theorem that uses it. A hypothesis sits in the statement, and anyone applying the theorem has to supply it or keep it as an assumption.

Writing the statement

Statements go wrong even in the benchmarks we use to measure autoformalization. An audit at ICML 2026 found 4,833 problems in five standard Lean benchmarks, 398 of them mechanically certified counterexamples, vacuous theorems or unsound axioms. These are the habits I use when I write a statement.

Start from the exact source, and write down every change. Every correction, strengthening, weakening and omission goes next to the Lean. Fixing a source and translating it are both fine as long as they're visible. FormalFlow's proof of a core theorem behind MIP* = RE corrected side conditions in the published argument and said so.
Use Mathlib's definitions, and test the ones you add. A wrong definition changes every theorem about it while every proof still goes through, so I give each new one a characterizing lemma, an example and a bridge to the standard notion. Mathlib's own definitions need reading too. The version I use has no P, NP or SAT, and Turing.TM2ComputableInPolyTime is relative to encodings you supply, so with constant encodings even the halting problem counts as polynomial-time.
Read the statement after elaboration. Mathlib gives its total operations values everywhere: Real.log 0 = 0, (2 : ℕ) - 3 = 0, and deriv (fun x : ℝ ↦ |x|) 0 = 0 even though |x| has no derivative at 0. A returned value doesn't establish the precondition, so the statement has to. Two traps come up on Zulip again and again. A bare ⊤ in ContDiff ℝ ⊤ f means analytic, not smooth, and a compactly supported analytic function on ℝⁿ is zero, so only the zero function qualifies. And autoImplicit is on by default in core Lean, even in files that import Mathlib, so π without open Real becomes an implicit variable instead of Real.pi. Turn it off, and look at statements with #check @name.
Try to break it before anyone proves it. A prover will happily use contradictory hypotheses and never touch the mathematics you meant. Find an input that satisfies all the hypotheses at once, check that every existential carries information, and make a target for an open problem say which side holds, since P ∨ ¬P is just Classical.em. VeriTile, a public Lean framework for Triton kernels, states two attention theorems under a hypothesis that fails for every positive shape, so they say nothing about any launch.
Don't trust equivalence checks once provers are strong. If you've proved P and you've proved Q, you've proved P ↔ Q without relating them at all. Poiroux and colleagues warned about this, and BEq+ was since measured accepting 94 to 96 percent of 50 unrelated provable pairs. My own habit is to turn a statement's fixed objects into parameters and try both readings on something simple, which is how the Yau gap at the top shows up.

An agent reads it first, then a person

Agents are good first readers. I hand one the elaborated statement with every definition it reaches, next to the paper it came from, and keep the proof out of sight. Then I ask for every place the two differ, an input where all the hypotheses hold, and a Lean-checked refutation. A refutation that fails proves nothing, but one that succeeds settles the question.

A doodle: the source and the statement with its definitions go to a robot holding a magnifying glass, with three questions: where do they differ, can the hypotheses hold, can you refute it. A dashed arrow labelled leads, not verdicts goes to a stick figure reading on their own. — What I hand a reader agent, and what I ask it for.

But agents are optimistic judges. Herald's judge rated Herald's own miniF2F translations 97.5 percent faithful, against 62.7 percent by human evaluation. So I treat what an agent says as a lead, and the person forms their own reading before looking at the agent's. A fresh agent that sees neither the source nor the proof can also back-translate the statement for a separate comparison, the way claimcheck does.

Saying what was proved

Autoinformalization gets much less attention, and I think it's where readers actually get misled. Thousands of people read a headline. A handful read the Lean behind it. When I reviewed openai/math, 76 of the 405 challenges sat under headlines that claimed more than their Lean, right next to a link to the Lean. One headline "resolves the uniform boundedness assertion in Hilbert's sixteenth problem" while the Lean covers quintic Liénard systems. The same release gets it right elsewhere: its SAT challenge proves (log log n)² in the exponent where the paper has log log n, and its docs say so. A gap stated like that costs nothing, and a headline that outruns the Lean costs the reader's trust in everything next to it.

Five levels of a formalization

Comparator says nothing about understanding. Kevin Buzzard asked the uncomfortable question on Zulip: if all we want is "a formal verification that a theorem is true", "then who cares about the art of proof?" I do. I believe the autoformalized proof matters too, not just the statement. For correctness it can come from anyone, but for understanding it can't. A formal proof that follows the paper checks the argument and not only the result, its lemmas are what other people reuse, and reading it is how you learn why the theorem is true. The Lean for OpenAI's Navier–Stokes blowup follows different bounds from its paper, so it checks the theorem, not the paper's argument.

So I think of five levels a formalization can aim at, roughly in order of the human time they take. The first two are correctness; the other three are understanding. None of them is wrong. The trouble starts when an artifact is announced at a level it hasn't reached, the way Atlas was.

A doodle of a five-step staircase: certificate, reviewed statement, readable project, reusable library and Mathlib, with correctness over the first two steps and understanding over the last three. A stick figure stands on step two, and a dashed orange arrow labelled Tau Ceti: skips 3? jumps from step two to step four. — Five levels, roughly in order of the human time they take.

Level 1, a certificate. One theorem, accepted by Comparator with the three standard axioms, and a proof nobody needs to read. The openai/math solutions are certificates for statements written by the same model that wrote the papers, and AxiomProver's IMO 2026 run proved statements it had autoformalized itself.
Level 2, a reviewed statement. The statement and its definitions have been read against the source, as in the checklist. Anthropic's FLT and Axiom's CFSG are both unread proofs, but of statements people wrote down first. FLT's challenge is Mathlib's own FermatLastTheorem, and its build fails unless #print axioms shows exactly the three axioms, a check anyone can copy with #guard_msgs. CFSG proves Tau Ceti's ClassificationStatement, whose exact Lean a human-reviewed roadmap gave in advance, although AIs implemented the groups it lists. Formal Conjectures and lean-eval are collections of such statements. This is the level the checklist gets you to.
Level 3, a readable project. You can learn the mathematics from it. A blueprint, made with leanblueprint or Verso's, ties the informal argument to Lean declarations and shows what is still open. Proofs are split into named lemmas and kept as short as the idea allows, with grind, omega or positivity doing the routine steps; Mathlib's review guide says golfing is fine "as long as it doesn't sacrifice readability". Public declarations have docstrings, and comments explain ideas instead of tactics. PFR, Carleson and Buzzard's FLT project are built around blueprints.
Level 4, a reusable library. Other people build on it, which is the hard half of the review guide: do the results already exist, "possibly in a more general form with a different name", does the code "provide a sensible API", and is it "general enough to support known future needs"? In practice that means definitions that fit Mathlib's hierarchy, names that follow its naming conventions, imports checked with lake shake, slow proofs measured with #count_heartbeats and fixed before anyone raises a limit, passing linters, and a library that survives a Mathlib bump. CSLib for computer science and PhysLib for physics, both built on Mathlib, aim here.
Level 5, Mathlib. Merged after maintainer review. The review guide orders the questions "approximately from easiest to hardest" as "style, documentation, location, improvements and library integration", and says the last one "generally requires several months of developing familiarity with mathlib". Mathlib also asks contributors to understand AI-written code well enough to justify each design decision "without the use of an AI".

Tau Ceti doesn't sit on the line, which is what makes it interesting. Humans write its roadmaps and review rubrics, AIs write and review the code, and its README says it is "explicitly not aiming here at curating and digesting mathematical knowledge in the way that a human authored library like Mathlib can". It skips the human reading of level 3 and goes for the reuse of level 4, and it's already reused as a source of statements, by Axiom's CFSG and some lean-eval problems. Whether reuse holds up when nobody reads the code is the experiment. Each level after the second takes more human time, and human time is what proof abundance doesn't give you.

Beyond mathematics

None of this is special to mathematics. The checklist and the levels apply as they are to theoretical computer science, physics and any field where a claim can be stated precisely, and the failures look the same everywhere: a quantifier in the wrong place, a hypothesis no input satisfies, a returned value read as a precondition. Code adds one thing. The statement is about a model of the program, its semantics, its harness and the machine it runs on, and somebody has to show that the model matches what ships. In a recent verification release, the LZO fuzz test checks only that decompression succeeds and returns the right length. The release notes say so, and the announcement describes more. That deserves a post of its own, so I'll leave it for another one.

Working with agents

The best systems I know share a loop: an informal plan, a split into lemmas, and lots of parallel proof search that reads Lean's error messages, from Aristotle's graph search to Maestro's coordinator, which can fix a false lemma using a counterexample Lean has checked. The column I care about in the table below is the last one, who wrote the statements, because that's where the difficulty is now. On MathAtlas, built from 103 graduate textbooks, strong baselines write a correct theorem statement at most 9.8 percent of the time.

Some agentic systems for Lean. Budgets and protocols differ widely, so this is not a ranking. Anthropic's FLT and Axiom's CFSG are on level 2 above.
System	Reported result	Statements by
AlphaProof	IMO 2024 P1, P2, P6 in Lean	experts, by hand
Aristotle	IMO 2025 P1, P3–P5 in Lean; P2 outside Lean	Harmonic, by hand
Four PutnamBench entries	672 of 672 (Aleph, NEAR AI, Forall, Humanfia), at reported mean costs of $0.17 to $74 a problem	benchmark authors (Aleph fixed 28, NEAR AI 2)
AxiomProver	Putnam 2025, 12 of 12 (8 in exam time); IMO 2026, 6 of 6	itself, for IMO 2026
Maestro	PutnamBench 669 of 672; IMO 2026, 6 of 6	benchmark authors; AxiomProver

Agents also change what they were asked to prove when it gets hard. In the xv6 verification, an agent that couldn't prove a lemma once deleted a line from the kernel source and once added an axiom, and the lemma turned out to be unprovable because the code had a bug. The agent that wrote the Axon compiler tried "unilaterally weakening the conclusion of the theorem". The cheating Jason Rute knew of was aimed at evaluations rather than at Lean's soundness: one model tried to look up the answers to a Lean benchmark, and another tried to call stronger models for help. Chris Bailey wasn't aware of any recent AI result that exploited a soundness bug.³

Separate writing from accepting. The agents that write statements, proofs and summaries shouldn't be the ones that accept them. Provers get read-only access to the frozen challenge, and every check runs outside their workspace.
Give the prover a way out. An agent that can say a statement is false, and have that handled separately from a failure, has less reason to cheat.
Report what you measured. Keep statement fidelity, proof completion and end-to-end success apart, say what the budget was and who wrote the statements, and test every gate on controls whose outcome you fixed in advance: a weakened statement, a contradictory hypothesis, a hole, an injected axiom.

Where to start

Tools for agents. The Lean REPL, Pantograph, the Kimina Lean Server, lean-lsp-mcp for agents that use the Model Context Protocol, and the Mathlib search engines LeanSearch, Loogle and LeanExplore.
Skills for coding agents. Cameron Freer's lean4-skills, with axiom checks and guardrails; Scott Armstrong's LeanAutoformalizationSkills, whose stated goal is to prove "the theorem the mathematical source actually states"; and Chris Birkbeck's mathlib-quality, for bringing agent-written code to Mathlib's standards.
Setups worth reading. mini-Lean-agent, which keeps the trusted evaluator apart from the prover, and SymCrypt's review of theorem statements before any proving.

Most of the habits here I learned from people in the Lean community.

There's also a PDF version with full references.

The excerpt compares only the growth conditions, so it says nothing about actual eigenfunctions. The full file compiles on Lean 4.35 with Mathlib, uses only the three standard axioms, and also proves that the paper's condition implies the challenge's. ↩
One of them is con-leche, whose verified mode is proved in Lean never to accept a theorem of False. ↩
Both from a recent Lean Zulip thread about press coverage of AI proofs (the thread), where Mario Carneiro's and Shreyas Srinivas's points above also come from. ↩