7 ms·

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 writt

by 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
    > Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem. Yes, this is what I understood. Thanks for confirming this point. > (And this concern doesn't apply if we already have the proof and just want to check it). Why this concern would not apply anymore if we already have the proof and just want to check it? The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq? (I understand this is a very rare occurence in practice and this is the reason why ZFC is so much used.)
    - lmm 12y ago
      > The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq? If Wiles' proof wasn't in ZFC we wouldn't call it a proof (at least not without qualification). You don't get to just write mathematical proofs in any language you like - otherwise we could pick a language in which FLT is an axiom, and then the proof of it is trivial.
      - ngrilly 12y ago
        I don't get it. There is a lot of variants of set theory. ZFC is just one of them, albeit the most common. But some proofs are founded on an extension of ZFC. For example, the Mizar system, which is another proof assistant, has adopted Tarski–Grothendieck set theory, an extension of ZFC. According to "The QED Manifesto Revisited" [1], it can be difficult to use Coq as-is for some kind of proofs: > Here are four mathematical statements that most mathematicians will consider to be totally non-problematic: [...] We claim that currently none of the QED-like systems can express all four statements in a good way. Of course one can easily extend the systems with axioms that allow one to write down these statements. However, that really amounts to ‘changing the system’. It would mean that both the library and the automation of the system will not be very useful anymore. Classical & extensional reasoning in Coq or abstract algebra in the HOLs by postulating the necessary types and axioms will not be pleasant without re-engineering the system. [1] http://mizar.org/trybulec65/8.pdf http://mizar.org/trybulec65/8.pdf

by thoran 12y ago

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
  > Yes, but only those that are undecidable in ordinary mathematics. If you're not using Coq, you have exactly the same problem. Yes, this is what I understood. Thanks for confirming this point. > (And this concern doesn't apply if we already have the proof and just want to check it). Why this concern would not apply anymore if we already have the proof and just want to check it? The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq? (I understand this is a very rare occurence in practice and this is the reason why ZFC is so much used.)
  - lmm 12y ago
    > The proof still needs to be expressed, directly or indirectly, in terms of Zermelo–Fraenkel set theory combined with first-order logic. If the proof uses a different and "incompatible" theory, how could we check it with Coq? If Wiles' proof wasn't in ZFC we wouldn't call it a proof (at least not without qualification). You don't get to just write mathematical proofs in any language you like - otherwise we could pick a language in which FLT is an axiom, and then the proof of it is trivial.
    - ngrilly 12y ago
      I don't get it. There is a lot of variants of set theory. ZFC is just one of them, albeit the most common. But some proofs are founded on an extension of ZFC. For example, the Mizar system, which is another proof assistant, has adopted Tarski–Grothendieck set theory, an extension of ZFC. According to "The QED Manifesto Revisited" [1], it can be difficult to use Coq as-is for some kind of proofs: > Here are four mathematical statements that most mathematicians will consider to be totally non-problematic: [...] We claim that currently none of the QED-like systems can express all four statements in a good way. Of course one can easily extend the systems with axioms that allow one to write down these statements. However, that really amounts to ‘changing the system’. It would mean that both the library and the automation of the system will not be very useful anymore. Classical & extensional reasoning in Coq or abstract algebra in the HOLs by postulating the necessary types and axioms will not be pleasant without re-engineering the system. [1] http://mizar.org/trybulec65/8.pdf http://mizar.org/trybulec65/8.pdf