zykarys

Blog / Systems

What "verified in Lean" does and doesn't buy you

A Lean proof guarantees the proof follows from the statement. It says nothing about whether the statement is the one you care about. AI-generated proofs make that gap the main event.

Systems3 min read

"Verified in Lean" is one of the strongest claims in computing, and one of the most misread. It guarantees less than people hear and more than skeptics admit. The useful work is in the gap.

What the check actually establishes #

Lean is a proof assistant. You write a formal statement — a theorem — and a proof. A small trusted core, the kernel, checks that every step of the proof follows from the rules of the logic and from definitions already accepted. If it accepts, the proof is correct relative to that statement, those definitions, and that kernel.

That is a remarkable guarantee. It's not "a reviewer looked at it and it seemed fine." It's mechanical, exhaustive, and repeatable by anyone who runs the checker. When a model produces a proof Lean accepts, you don't need to trust the model at all for that step.

So far, so good. Now read the guarantee again and notice its shape: correct relative to the statement.

The statement is where the trust moved #

A Lean proof proves exactly what the formal statement says. If the statement is subtly different from the claim you care about, the proof is a perfect answer to the wrong question.

This is the specification gap, and it's old news in formal methods. What's new is that AI changes who writes which part. When a human mathematician formalizes a theorem, the hard creative work is the proof, and the statement is usually a careful translation by the same person. When a model generates a proof, the proof becomes cheap and checkable. The statement becomes the place where an error can hide.

Here are the ways a formal statement can drift from the intended claim:

  • A hypothesis that's too strong. Assume something false or vacuous and you can prove anything. A theorem whose premises can never be satisfied is true and useless.
  • A definition that doesn't mean what its name says. A function called is_sorted that checks something slightly different. Lean will happily prove facts about it.
  • A conclusion that's weaker than advertised. Proving a bound exists instead of proving the specific bound, or proving a property for one case instead of all.
  • Escape hatches. Lean lets you postulate axioms or leave a gap with a placeholder like sorry. A careful checker flags these, but a headline won't.

None of these is a flaw in Lean. All of them are reasons "verified in Lean" can be true while the claim people repeat is false.

The trust base, spelled out #

When I read "verified in Lean," I translate it into a list of things I'm being asked to trust:

  1. The kernel is correct. Small, heavily scrutinized, and the strongest link.
  2. No extra axioms were added beyond the standard ones, and no placeholders remain.
  3. The library definitions used — often from Mathlib, Lean's community math library — mean what I think they mean.
  4. The formal statement matches the informal claim.

Item 1 is nearly free. Items 2 and 3 are cheap to check if the proof is published. Item 4 is the expensive one, and it can only be checked by a person who understands both the mathematics and the formalization.

So here's the rule: a "verified" claim without the formal statement published next to the informal one is a claim you can't evaluate. The proof can be a thousand lines; the statement is usually a few. Show me the few.

Why this matters beyond math #

The same structure shows up anywhere AI output is checked by a machine. Unit tests prove code satisfies the tests, not the requirements. A type checker proves types line up, not that the program does the right thing. Every automated check moves trust from the artifact to the specification it's checked against.

That's not an argument against automated checking. It's an argument for putting human attention where the trust went. If proofs are cheap and checking is free, then reviewing statements is the job.

What to watch #

Expect a pattern: announcements that an AI system "proved" a result, followed days later by experts noting the formal statement was narrower than the headline. If those corrections become rare because labs start publishing statements alongside claims and inviting review before the press release, the gap is closing. I'd count that as real progress, more than any single proof.