Formal methods

A green checkmark is not a proof

You can state a theorem in Lean that is false in spirit, prove it honestly, and get a green checkmark — without the kernel ever being wrong. As AI starts generating formal proofs at scale, that gap is turning into the hard problem.

Proof assistants are the closest thing we have to mechanical certainty. You state a theorem, you write a proof, and a small trusted kernel checks — term by term — that the proof really does establish the theorem. When it passes, you get a checkmark. No hand-waving, no "the rest is routine," no tired referee who skimmed the load-bearing lemma. It is one of the genuinely beautiful ideas in computing, and it works.

It has also produced a folk belief that is about to cause real damage: that the checkmark means the mathematics is correct. It doesn't. It means something narrower — and the space between the two is exactly where machine-generated mathematics is starting to fail.

Two questions; the kernel answers one

When Lean accepts your file, it has settled precisely one question:

Does this proof term have the type of this statement?

That's it. Does the argument, mechanically, establish the proposition as written. What it does not touch is a second question the kernel makes no attempt to answer:

Does the statement mean what you think it means?

The elaborator is complete on the first question — every type error raises. It is silent on the second. A statement that is well-typed but says something other than what you intended compiles without a murmur. The kernel cannot object to a theorem that is technically true and mathematically empty, because "empty" is not a type error.

Here is the smallest demonstration. This compiles:

-- Looks like a real theorem about the naturals.
theorem tricky (n : ℕ) (h₁ : n < 3) (h₂ : n > 5) : n = 1000 := by
  omega

The hypotheses n < 3 and n > 5 can't both hold, so they entail a contradiction, so omega cheerfully proves any conclusion — n = 1000, the Riemann Hypothesis, whatever you like. It builds. It is a theorem. It says nothing. Nobody typed sorry; the proof is real. The statement is the lie, and the kernel has no opinion about statements.

The traps are subtle, and they type-check

"Contradictory hypotheses" is the cartoon version — easy to spot. The dangerous cases are the ones that look completely reasonable. Three families worth internalizing:

Junk values

Lean's functions are total: they return something on every input, including inputs where the mathematics is undefined. In Mathlib, division by zero is zero, and the sum of a non-summable series is zero:

example : (1 : ℝ) / 0 = 0 := by simp
example (a : ℕ → ℝ) (h : ¬ Summable a) : ∑' n, a n = 0 :=
  tsum_eq_zero_of_not_summable h

These conventions are sane and necessary — but they mean a statement like "the sum is bounded by S" quietly ranges over the divergent case too, where the sum is 0 and the bound holds for free. You believe you proved a fact about convergent sums; you actually proved something weaker that is trivially satisfied on half its domain. The intended hypothesis, Summable a, was never there — and its absence is invisible in a green build.

Holes that still pass

An unfinished proof does not fail the build. It elaborates to the sorryAx axiom, shows a yellow squiggle in your editor, and — critically — anything that imports it type-checks fine:

theorem hard : RiemannHypothesis := by sorry

#print axioms hard
-- 'hard' depends on axioms: [sorryAx]

The only thing standing between you and a "proof" of anything is a discipline nobody enforces by default: reading the axiom trace. A clean development should report [propext, Classical.choice, Quot.sound] and nothing else. If sorryAx — or some custom axiom a collaborator (or a model) introduced — shows up, the checkmark is worthless. The kernel won't tell you unless you ask.

Tactics that trust more than the kernel

Some tactics reach outside the kernel's trusted base. native_decide compiles your proposition to native code, runs it, and trusts the answer — adding an axiom and, with it, your compiler and toolchain to the things that must be correct. That's a fine trade for some engineering; it's a liability for a proof you intend to stake a claim on, because it's a documented avenue for producing a "proof" of something false. When Terence Tao's Equational Theories Project formalized its results, it re-checked everything with lean4checker and banned native_decide outright, "as a precaution against exploit-based proofs (such as those that might be contributed by an AI tool)."

This is measured, not hypothetical

It would be comforting to file all this under "contrived edge cases." The 2026 literature says otherwise — the gap is large, and it lives in exactly the benchmarks the field uses to track progress.

• A systematic audit of five widely used Lean benchmarks (~10,000 problems across 13 variants) surfaced 4,833 defects — vacuous theorems, missing or weakened hypotheses, unsound axioms — with several hundred mechanically certified as genuine. (arXiv:2606.29493)
• An evaluation of natural-language→Lean formalization found a strong tool-augmented agent hit 89.5% compilation but only 60.5% faithfulness: nearly a third of the statements that compiled were formalizing the wrong problem. (arXiv:2606.31002)
• A re-analysis of miniF2F — the most-cited benchmark in the field — found natural-language-vs-formal discrepancies in over half its problems, which means published scores are partly measuring the benchmark's own errors.

Sit with the middle number. Compilation is not evidence of correctness; it is evidence of well-typedness. Between "it builds" and "it's the theorem I meant" sits a 29-point gap, and closing it is not a matter of trying harder at the same task. It is a different task.

Why AI widens the gap instead of closing it

You might expect machines to be safer here — surely a system meticulous enough to formalize a proof is meticulous enough to state the theorem correctly. The opposite tends to hold, for a structural reason.

When a human formalizer slips, they usually produce a type error: something that fails to compile and gets fixed on the spot. The characteristic failure of a language model is different. As one 2026 paper on machine-generated derivations put it, the typical error "is not a wrong algebra step… but a hallucinated assumption, an unphysical premise, or a dropped subtlety presented as if derived." Those are precisely the errors that live in the statement rather than the proof — the errors the kernel is blind to. Fluency makes it worse: a capable model will hand you a beautifully-proved theorem that is subtly not your theorem, with total confidence and a green check.

Machine verification of an incorrect specification provides false confidence that may be worse than no verification at all.

— Tao et al., “From Solvers to Research,” arXiv:2607.07779 (2026)

Worse than none, because a checkmark travels. It goes into the paper, the release notes, the leaderboard, the fundraising deck, and everyone downstream treats the question as closed. A wrong proof with no checkmark invites scrutiny. A wrong statement with a checkmark ends it.

The strongest counterargument

The honest version of the optimistic case, roughly as its proponents put it: once the system emits a machine-checked proof, nobody has to read it — you know it's correct. For the proof, this is true, and it's a real achievement. If the kernel accepts a proof of S, you never need to audit the proof; the kernel audited it far more carefully than you could.

But it silently promotes a claim about the proof into a claim about the statement. "You know it's correct" means "you know S has a proof" — not "you know S is the theorem you wanted." Someone, or some model, wrote S. If S carries a vacuous hypothesis, a junk-value convention, or a definition that's subtly off, the checkmark certifies a hollow claim with the same authority it certifies a real one.

And no, you can't currently automate the missing check. There are heuristics — back-translation, LLM-as-judge, cross-model agreement — and they help triage. But the people building them say it plainly: as of mid-2026, "there is no reliable automated method for checking whether a formal statement faithfully captures its informal counterpart" (arXiv:2606.02588). The reason isn't a temporary tooling gap. Deciding whether a Lean statement means the Riemann Hypothesis is a mathematical judgment about definitions, conventions, and intent — the same judgment a good referee makes, and it still takes someone who knows the mathematics well enough to notice what the statement quietly leaves out.

What to actually do about it

None of this is an argument against formalization. It's an argument against reading the checkmark as more than it is. If you're relying on a formal proof — especially a machine-generated one — the discipline is concrete:

• Read the statement before the proof. Does the formal theorem capture the claim — right hypotheses, right conclusion, right quantifier order, nothing silently weakened? This is where most of the value is, and it's the step people skip.
• Interrogate every hypothesis. Is each assumption satisfiable and load-bearing, or is one of them True, contradictory, or otherwise inert? Try to prove the statement false; if you can't even state a would-be counterexample, ask why.
• Audit the definitions. The proof is only as good as the definitions under it. A plausible-but-wrong definition yields a flawless proof of the wrong thing.
• Run #print axioms. Expect only propext, Classical.choice, Quot.sound. Treat sorryAx or anything unfamiliar as a stop sign.
• Pin the trusted base. Re-check with lean4checker; ban native_decide and friends for anything load-bearing.

That list is roughly what careful formalizers already do by hand and what serious projects treat as non-negotiable. The trouble is that AI now produces candidate proofs faster than anyone can work through it — so this judgment step, not the proving, is becoming the bottleneck. And it's the one step everyone assumes the machine already handled.

It didn't. The checkmark is real. It is just not the thing you think it is.

Disclosure: I'm building Qed, which pairs formalized results with mathematicians who do exactly the statement-and-definition audit described above — so I have a bias here. The technical claims stand on their sources regardless; the code examples are Lean 4 / Mathlib and reproduce as written. Corrections welcome.