Learn · Intermediate
Proof assistants: why a machine-checked proof beats a convincing one
A proof assistant is a piece of software -- the best known are Lean and Coq -- that checks a mathematical proof one step at a time against strict logical rules and accepts it only if every single inference holds. The point is certainty: a proof that a proof assistant verifies is essentially guaranteed to be logically correct, with no hidden gaps. That is exactly why, when OpenAI claimed its AI proved a 50-year-old conjecture, the mathematical community's first demand was not applause but "show us the Lean or Coq proof."
To see why that demand is so insistent, you have to appreciate the difference between a proof that is convincing and a proof that is correct. A traditional math proof is a piece of persuasive writing aimed at other experts: it makes a series of claims, and a human referee reads along, nodding, checking that each step follows. This works remarkably well, but it has a failure mode -- a proof can look completely convincing and still contain a subtle error that even careful referees miss. The history of mathematics includes famous "proofs" that stood for years before a gap was found. Persuasiveness is not correctness.
A proof assistant closes that gap by refusing to take anything on faith. You rewrite the proof in a formal language the software understands, breaking every argument down to inferences so small and explicit that a computer can verify each one mechanically. There is no "clearly" and no "it is easy to see that" -- every one of those hand-waves has to be filled in until the chain of reasoning connects, atom by atom, from the accepted axioms to the conclusion. If a single link is missing, the assistant rejects the proof and points at the gap. It cannot be charmed, rushed, or fooled by an argument that merely sounds right. The analogy is the difference between a persuasive lawyer convincing a tired jury and a formal audit that checks every transaction against the ledger: one appeals to judgment, the other leaves nothing to it.
This is precisely the property that matters when the author of a proof is a language model. A large language model generates text that is statistically plausible -- and a proof that mimics the structure and cadence of a valid argument is exactly the kind of plausible text these models are good at producing, whether or not the logic underneath is sound. That is the mathematical version of a hallucination: a fluent, authoritative-looking argument with a fatal hole. A three-page PDF from an AI is, to a mathematician, just text until something checks it. Run that same proof through Lean, and if it compiles, the debate about its logical validity is essentially over. This is why formal verification has become the gold-standard evaluation for AI reasoning about mathematics -- it converts "trust me" into "check it yourself, mechanically."
There is an important limit, and it is easy to miss. A proof assistant guarantees that the proof of a statement is valid; it does not guarantee that the statement is the one you meant. If you formalize the wrong theorem -- subtly misstate the hypotheses, say -- the assistant will happily verify an airtight proof of something nobody cares about. So human judgment does not disappear; it moves. Instead of checking every step, experts check that the formal statement faithfully captures the real claim, and then let the machine handle the steps. This is a genuinely good division of labor: humans are good at meaning, machines are good at not skipping steps.
Why this matters beyond mathematics: proof assistants are the sharpest available test of whether an AI system is actually reasoning or merely producing reasoning-shaped text. As models get better at long, multi-step problem solving -- the kind of deliberate test-time compute and agentic loops now used to attack hard problems -- the risk of confident, wrong-but-plausible output grows, not shrinks. The exciting frontier is AI that does not just write a proof but writes it directly in Lean, so the model's output arrives pre-verified. Systems like DeepMind's geometry and olympiad provers already work this way, generating formally checked proofs rather than prose. That is the standard the field is converging on: for a machine's claim of a mathematical breakthrough, the proof is not the PDF -- the proof is the code that a proof assistant will confirm.
Key questions
What is a proof assistant?
Why do mathematicians want a Lean or Coq proof when an AI claims to prove a theorem?
If a proof assistant checks the proof, is human review no longer needed?
Cite this
APA
Ground Truth. (2026, July 10). Proof assistants: why a machine-checked proof beats a convincing one. Ground Truth. https://groundtruth.day/learn/what-is-a-proof-assistant.html
BibTeX
@misc{groundtruth:what-is-a-proof-assistant,
title = {Proof assistants: why a machine-checked proof beats a convincing one},
author = {{Ground Truth}},
year = {2026},
month = {jul},
url = {https://groundtruth.day/learn/what-is-a-proof-assistant.html}
}