6 ms·

See, for example: https://en.wikipedia.org/wiki/Wiles%27_proof_of_Fermat%27s_Last_Theorem https://en.wikipedia.org/wiki/Wiles%27_proof_of_Fermat%27s_L... http

See, for example: https://en.wikipedia.org/wiki/Wiles%27_proof_of_Fermat%27s_Last_Theorem https://en.wikipedia.org/wiki/Wiles%27_proof_of_Fermat%27s_L... http://rsta.royalsocietypublishing.org/content/roypta/363/1835/2401.full.pdf http://rsta.royalsocietypublishing.org/content/roypta/363/18...

lmm 12y ago
Wiles' proof was not written in machine-checkable language; if it had been, the error would almost certainly have been caught.
- ngrilly 12y ago
  But writing Wile's proof in a machine-checkable language wouldn't have been a problem in itself? There is no "universal" machine-checkable language which can be used for any proof. I don't know if Wiles' proof could have been written in Coq, for example. Let's say it can't, and that no existing machine-checkable language can be used for this purpose. In such a case, you would have to develop a new proof language, and make sure the proof checker itself is correct. I guess that at some point we are hitting the theoretical limits imposed by the halting problem and Gödel's incompleteness theorems? It's not my field so I'm just asking questions here. Don't hesitate to lecture me :-)
  - thoran 12y ago
    No, you're wrong. This is not a theoretical issue there, but a practical one. Almost all mathematics (and this certainly includes Wile's proof) could be written in Coq, in theory. It is extremely hard to do in practice. Mathematicians write proof for their peers who have a smart brain. Most of the trivial and less than trivial details are omitted. Coq cannot not accept this (because he is very stupid and can't figure the missing steps). It turns out that it is particularly hard and boring to fill the missing holes in a "human" proof. Gödel comes in when you try to prove Coq's correctness within Coq (but this was partially done, in a sense)
    - ngrilly 12y ago
      I want to make sure I understand correctly. :) I am right on the fact that rewriting Wile's proof in a machine-checkable language is a problem in itself? But I'm wrong when I suggest it is theoretical issue, when it's actually practical issue? I've read that "the theory behind Coq is generally admitted to be consistent with regard to Zermelo-Fraenkel set theory + inaccessible cardinals". [1] I also read that some statements are undecidable in Zermelo–Fraenkel set theory [2]. It follows from this that it must exist some statements that are undecidable in Coq, correct? But I understand that this is theoretical issue, not a practical one, because "Zermelo–Fraenkel set theory, combined with first-order logic, gives a satisfactory and generally accepted formalism for essentially all current mathematics". Is it the reason why my comment was wrong? On this topic, I've read an article titled "Computer verification of Wiles' proof of Fermat's Last Theorem" which explains that Wile's proof could probably be verified with a tool like Coq, but that would be a massive challenge: > The mathematics used in Wiles' proof of Fermat's Last Theorem is very complicated. [...] I do not know the provers Coq and Mizar good enough, but I think they are adequate to express the mathematics. > On the other hand, I do think that the challenge is doable, and that it will be done in the coming fifty years. It is definitely not within reach. The project will have to cover large parts of current pure mathematics. Its scope is comparable with the Bourbaki project, where between 1950 and 1970 almost all of pure mathematics got a new foundation by the efforts of an originally French group of mathematicians who published some 20 books under the pseudonym N. Bourbaki. [1] https://coq.inria.fr/faq https://coq.inria.fr/faq [2] http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_th... [3] http://en.wikipedia.org/wiki/Hilbert%27s_program http://en.wikipedia.org/wiki/Hilbert%27s_program [4] http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html
      - lmm 12y ago
        > It follows from this that it must exist some statements that are undecidable in Coq, correct? Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem. (And this concern doesn't apply if we already have the proof and just want to check it).
- ngrilly 12y ago
  According to my very fresh reading on this topic, you are right, but your comment give the impression that writing Wile's proof in a machine-checkable language is not very different from writing it in a human language. According to this article, I understand it is a lot more difficult to write a proof in a machine-checkable language, in the current state of the art: http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html I read a lot of comments on Hacker News and Lobsters saying "you could have avoided this bug by writing your program in Idris, Coq, Haskell, etc. and enjoying the benefits of the Curry-Howard Isomorphism". But I'm under the impression that most of this comments undervalue the effort in "feeding" the type/proof checker with the necessary formalism. I'm not saying that establishing a proof is worthless. Of course there is a lot of value in having a formal proof. I'm just saying that even for full-time professional mathematicians, machine-checkable formal proofs are still the exception, not the norm. This suggests the cost of building these proofs is still high, and it may explain why the practice is still limited in the field of computer science.

lmm 12y ago

Wiles' proof was not written in machine-checkable language; if it had been, the error would almost certainly have been caught.

ngrilly 12y ago
But writing Wile's proof in a machine-checkable language wouldn't have been a problem in itself? There is no "universal" machine-checkable language which can be used for any proof. I don't know if Wiles' proof could have been written in Coq, for example. Let's say it can't, and that no existing machine-checkable language can be used for this purpose. In such a case, you would have to develop a new proof language, and make sure the proof checker itself is correct. I guess that at some point we are hitting the theoretical limits imposed by the halting problem and Gödel's incompleteness theorems? It's not my field so I'm just asking questions here. Don't hesitate to lecture me :-)
- thoran 12y ago
  No, you're wrong. This is not a theoretical issue there, but a practical one. Almost all mathematics (and this certainly includes Wile's proof) could be written in Coq, in theory. It is extremely hard to do in practice. Mathematicians write proof for their peers who have a smart brain. Most of the trivial and less than trivial details are omitted. Coq cannot not accept this (because he is very stupid and can't figure the missing steps). It turns out that it is particularly hard and boring to fill the missing holes in a "human" proof. Gödel comes in when you try to prove Coq's correctness within Coq (but this was partially done, in a sense)
  - ngrilly 12y ago
    I want to make sure I understand correctly. :) I am right on the fact that rewriting Wile's proof in a machine-checkable language is a problem in itself? But I'm wrong when I suggest it is theoretical issue, when it's actually practical issue? I've read that "the theory behind Coq is generally admitted to be consistent with regard to Zermelo-Fraenkel set theory + inaccessible cardinals". [1] I also read that some statements are undecidable in Zermelo–Fraenkel set theory [2]. It follows from this that it must exist some statements that are undecidable in Coq, correct? But I understand that this is theoretical issue, not a practical one, because "Zermelo–Fraenkel set theory, combined with first-order logic, gives a satisfactory and generally accepted formalism for essentially all current mathematics". Is it the reason why my comment was wrong? On this topic, I've read an article titled "Computer verification of Wiles' proof of Fermat's Last Theorem" which explains that Wile's proof could probably be verified with a tool like Coq, but that would be a massive challenge: > The mathematics used in Wiles' proof of Fermat's Last Theorem is very complicated. [...] I do not know the provers Coq and Mizar good enough, but I think they are adequate to express the mathematics. > On the other hand, I do think that the challenge is doable, and that it will be done in the coming fifty years. It is definitely not within reach. The project will have to cover large parts of current pure mathematics. Its scope is comparable with the Bourbaki project, where between 1950 and 1970 almost all of pure mathematics got a new foundation by the efforts of an originally French group of mathematicians who published some 20 books under the pseudonym N. Bourbaki. [1] https://coq.inria.fr/faq https://coq.inria.fr/faq [2] http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_th... [3] http://en.wikipedia.org/wiki/Hilbert%27s_program http://en.wikipedia.org/wiki/Hilbert%27s_program [4] http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html
    - lmm 12y ago
      > It follows from this that it must exist some statements that are undecidable in Coq, correct? Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem. (And this concern doesn't apply if we already have the proof and just want to check it).
ngrilly 12y ago
According to my very fresh reading on this topic, you are right, but your comment give the impression that writing Wile's proof in a machine-checkable language is not very different from writing it in a human language. According to this article, I understand it is a lot more difficult to write a proof in a machine-checkable language, in the current state of the art: http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html I read a lot of comments on Hacker News and Lobsters saying "you could have avoided this bug by writing your program in Idris, Coq, Haskell, etc. and enjoying the benefits of the Curry-Howard Isomorphism". But I'm under the impression that most of this comments undervalue the effort in "feeding" the type/proof checker with the necessary formalism. I'm not saying that establishing a proof is worthless. Of course there is a lot of value in having a formal proof. I'm just saying that even for full-time professional mathematicians, machine-checkable formal proofs are still the exception, not the norm. This suggests the cost of building these proofs is still high, and it may explain why the practice is still limited in the field of computer science.