Discovery & AI
Proofs a Computer Can Check
Also called: Formal verification
- Established idea
- Formal theory
- Working interpretation
A proof-checking program, or another independent checker, raises the bar from an argument that sounds right to logic where every step can be tested. Checking is how I earn confidence in a result, not a badge to decorate it with.
Could someone else rebuild this argument and check it on their own?
Why it attracts me
Verification is a way to earn confidence, not a badge to decorate a result. I like that a proof checker cannot be charmed. It ignores how elegant the explanation is and how confident the author sounds.
The idea
In ordinary mathematics, a proof is written for human readers, who fill small gaps themselves. In formal verification, the proof is written so that a program can check every step against exact definitions. If any step fails, the proof is rejected. This makes the difference between a convincing demonstration and a proof impossible to miss, which is the line Proof Versus Evidence is about.
An example
In my Agentic Maths side quest, the strongest result is a construction that works for every size from 17 upward. Its main theorem, and the 351 smaller worked cases the proof builds on, are confirmed by Lean's core checker. The page still marks it as ready for expert review, not peer reviewed. Another result there carries a warning about which reading of the original problem it answers. That is a gap no checker can close: it confirms the proof, not that the statement matches what people meant.
What I think (and don't know)
Machine checking pairs naturally with AI-led discovery (AI Systems That Discover, Not Just Summarize), because AI can write fluent arguments that are wrong. What I do not know is how much of real mathematics can be formalized at a reasonable cost. Checking a proof and attacking a claim with hostile tests (Trying Hard to Break My Ideas) are different tools, and I want both.
What this does not establish
A computer-checked proof shows that the conclusion follows from the stated definitions. It does not show that those definitions capture the question people actually care about, or that the result is new or important.
Questions I'm still exploring
- How can I be sure the formal statement says what the original question meant?
- When is a full machine-checked proof worth the extra effort?
- How should a checked proof be explained so that people, not only programs, understand it?
Sources and further reading
- Lean, an open-source programming language and proof assistant
- Thomas Hales et al., "A formal proof of the Kepler conjecture", Forum of Mathematics, Pi 5 (2017): e2 — A famous case where a long, computer-assisted proof was later fully checked by proof assistants.
Working interpretation: drafted from my notes and interests for review. It is not a direct quotation, and I may still change it.