[Turneyboy]

The nice thing about formal verification is exactly that. You have a separate tool that's very much like a compiler that can check those 1200 pages and tell you that it's true.

The source of truth here is the code we wrote for the formal verification system.

[gosub100]

Could formal verification prove the nexus between the Taniyama-Shimura conjecture and Fermat's last theorem? I don't claim to know what the former is, but I am skeptical that a system that can only validate what we already know would have any luck with sudden leaps between disparate corners of the field. Or worse, what if we had this verification 30 years ago, Wiles gets excited thinking he proved a 300 year old mystery, only to be told by the algorithm, "sorry son, this code doesn't verify. Try again next time!"

[falcor84]

> "sorry son, this code doesn't verify. Try again next time!"

But that's not how it works; rather it tells you about the specific issue with a particular step in the proof, which you then debug, as you would with code that isn't compiling (or not passing some static analysis test).