|
|
|
|
|
|
by gosub100
578 days ago
|
|
|
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!" |
|
|
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).