Computer-Assisted Proof Verification

Intro to Proofs · Axiom Academy

Computer-Assisted Proof Verification Software that controls an aircraft can't have a hidden bug. So how do we make a computer check a mathematical proof with absolute certainty — and prove the software is right? In 1994 , Andrew Wiles' proof of Fermat's Last Theorem had a gap that took a year to find. For pure math that's frustrating — but the same logic now runs flight-control software , where one missed step can be fatal. Let's build the tool that catches it. A proof assistant reads every single line Here's a real proof — "if n is even, then n ² is even" — written as separate steps. Step the checker down it: it accepts a line only when it follows by a rule. Then flip inject a gap and watch where it stops. Why not just have more mathematicians check it? Human review is good — but on a long proof, the chance that every reviewer misses one subtle flaw grows fast. Drag the proof length and compare: human review vs. a machine that checks every step with certainty. Where it ships: proving software for all inputs Aircraft control code has too many possible inputs to test them all — there are simply too many combinations. Drag the number of test cases, watch how little of the space you cover, then flip formal proof : it covers everything at once. That's how the CompCert compiler is certified for Airbus.

This is the written version of the interactive lesson above. See the full Intro to Proofs course.