4 ms·
>denying the legitimacy of computer-generated proofs protects their livelihood/careers. While this might be an issue, the bigger problem is that there are no i
by tacomonstrous 8y ago
>denying the legitimacy of computer-generated proofs protects their livelihood/careers.
While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet.
What is true is that there is still serious prejudice against theorems verified by reducing to a finite (yet large) number of concrete cases, which are then verified by an algorithm. This is the case even after the whole brouhaha over and resolution of the 4 colors theorem by Hales.
- dannykwells 8y agoGood catch on the generated vs. assisted - I edited my comment.
- auggierose 8y agoHales didn't resolve the 4 colors theorem, Gonthier did that. Hales proved the Kepler Conjecture and afterwards facilitated its formal verification via the Flyspeck project.
- wolfgke 8y ago> Hales didn't resolve the 4 colors theorem, Gonthier did that. Gonthier didn't resolve the 4 colors theorem, Appel and Haken did that. Gonthier just created the first computer-checked proof for the Four-color theorem.
- tacomonstrous 8y agoYes, thank you. Mixed up machine assisted proofs.
- dwheeler 8y ago>> denying the legitimacy of computer-generated proofs protects their livelihood/careers. > While this might be an issue, the bigger problem is that there are no interesting new theorems that were obtained in this way yet. I think the issue is that there is a need for computer verified proofs, not necessarily computer generated proofs. It's much easier to create a proof verifier than a proof generator, and verifiers can give us much greater confidence that the proofs are correct (regardless of whether a human or computer generated them).