8 ms·

In science it may happen because everything is based on a lot of assumptions, themselves based on our physical perception of the world, which may be proved wron

by arcatek 12y ago

In science it may happen because everything is based on a lot of assumptions, themselves based on our physical perception of the world, which may be proved wrong later in time. Are mathematics subject to this kind of flaws ? There is a very restricted set of axioms, and almost everything else is based on formal proofs.

Drakim 12y ago
Surely the implementation of the mathematics may be subject to errors, just like any implementation of anything? There is nothing that is so perfect that humans cannot err while applying it.
- scscsc 12y ago
  It is true that there might be errors in anything. However, this is mitigated by having only a very small core that checks the proofs. Basically if there if a wrong proof goes through, there must be an error in the core (which was checked by many people and is very small).
  - vertex-four 12y ago
    You have to translate between the English spec and the computer-readable proof, and surely it's relatively easy to mess that up in some way and end up proving the wrong thing.
    - qznc 12y ago
      The C spec and x86 assembly are two very well known specs.
      - vertex-four 12y ago
        If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. I don't doubt that formal verification significantly reduces the chances of bugs, but it's not a panacea, or we have computers that read our minds. You still need to verify that the proof is proving the right thing, although you can be sure that it's internally consistent.
        more_original 12y ago
        > If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're verifying the compiler from one language to the other. The specifications of the two languages are not that hard to implement. The difficulty is covering all cases in compiling from one to the other. The formal proof does tell us that we haven't missed any.
  - Drakim 12y ago
    I agree that the chances are pretty small, but is that "good enough" when it comes to formally verifying things? (I know next to nothing about formal verification)
    - scscsc 12y ago
      Well, that's also true. But apparently there is no better thing to do. There is always a disconnect between what you mean and what you say. It happens all the time and the risk is not going to go away. People who work with proof assistants understand this risk better and most of them are pretty happy that the risk is sufficiently small for their purposes.
one-more-minute 12y ago
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)
      - 12y ago

by arcatek 12y ago

Drakim 12y ago

Surely the implementation of the mathematics may be subject to errors, just like any implementation of anything? There is nothing that is so perfect that humans cannot err while applying it.

scscsc 12y ago
It is true that there might be errors in anything. However, this is mitigated by having only a very small core that checks the proofs. Basically if there if a wrong proof goes through, there must be an error in the core (which was checked by many people and is very small).
- vertex-four 12y ago
  You have to translate between the English spec and the computer-readable proof, and surely it's relatively easy to mess that up in some way and end up proving the wrong thing.
  - qznc 12y ago
    The C spec and x86 assembly are two very well known specs.
    - vertex-four 12y ago
      If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. I don't doubt that formal verification significantly reduces the chances of bugs, but it's not a panacea, or we have computers that read our minds. You still need to verify that the proof is proving the right thing, although you can be sure that it's internally consistent.
      - more_original 12y ago
        > If they're very well known and everyone can understand them and implement them perfectly, we wouldn't need formal verification in the first place. We're verifying the compiler from one language to the other. The specifications of the two languages are not that hard to implement. The difficulty is covering all cases in compiling from one to the other. The formal proof does tell us that we haven't missed any.
- Drakim 12y ago
  I agree that the chances are pretty small, but is that "good enough" when it comes to formally verifying things? (I know next to nothing about formal verification)
  - scscsc 12y ago
    Well, that's also true. But apparently there is no better thing to do. There is always a disconnect between what you mean and what you say. It happens all the time and the risk is not going to go away. People who work with proof assistants understand this risk better and most of them are pretty happy that the risk is sufficiently small for their purposes.

one-more-minute 12y ago

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)
    - 12y ago