5 ms·

I have a question about these hundreds-of-pages long proofs. Who can check such long proofs and be confident about it? To study a document of this size and adva

by Kenji 11y ago

I have a question about these hundreds-of-pages long proofs. Who can check such long proofs and be confident about it? To study a document of this size and advanced content rigorously, you would need years - and even then, it is not certain that you didn't overlook something. How can I ever be confident in such proofs until they are checked in, say, Coq or something?

kirrent 11y ago
In this case, each chapter of the proof was sent off to different people so they could spend time studying a smaller section of the proof. Famously a significant mistake was discovered during this review that took Wiles a year to fix.
7373737373 11y ago
I have the same questions when reading something like this. Expert verification seems more like an appeal to authority and intuition instead of a definite proof with formal rigorosity. Locally, there is always structure, but in pure mathematics even these steps require such an in depth understanding that trusting experts as an outsider seems to be impossible, it could as well be magic. As a programmer, I have a quite mechanistic understanding of the world, projects like http://us.metamath.org/index.html http://us.metamath.org/index.html seem to make it much more understandable. I'm wondering, if the longest path to the theorem "2 + 2 = 4" is 150 layers deep in this system, how deep would this proof be?
StefanKarpinski 11y ago
This is one of the reasons it takes a lot of training and talent to become a mathematician. If you wonder how mathematicians can do this when programmers write such buggy programs and the two processes seem so similar, I would note that I've found that mathematicians are remarkably careful, if slow, programmers and they make mistakes at a much lower rate than most programmers. If you consider moreover that mathematics is entirely free of many of the things that make programming hard – such as any kind of mutable state, input/output or concurrency – then you can see why proof may be a more reliable process than programming. Another part of is that one spends a huge amount of time questioning and testing every single step of a proof. There's a slow back-and-forth process to proving things: 1. I think this is true – let me try to prove it. 2. I get stuck on something in the proof – let me try to construct a counterexample to the specific thing I'm currently trying to prove. 3. If I can't construct a counterexample, why? That reason itself is a proof of the point I was stuck on. And so on, back-and-forth until the whole proof is done or you've managed to find some insane, devious counterexample. So by the time you've proved something, you've looked at it from every angle and considered every possibility. Mathematicians reading a proof do something very similar, but a bit more passively – it's still a very active process where you try to poke holes in every single claim and convince yourself that you can't before moving on. But a lot of the steps will be completely obvious to a trained mathematician – it's the sequence of them that's non-obvious, but once presented in order, the arc of reasoning becomes crystal clear and irrefutable.
comex 11y ago
Huh, I thought I had read somewhere that a machine checked proof of Fermat's Last Theorem had already been created. I must have mixed it up with something else.
- GFK_of_xmaspast 11y ago
  Are you thinking of Fermat's Little Theorem?

by Kenji 11y ago

kirrent 11y ago

In this case, each chapter of the proof was sent off to different people so they could spend time studying a smaller section of the proof. Famously a significant mistake was discovered during this review that took Wiles a year to fix.

7373737373 11y ago

I have the same questions when reading something like this. Expert verification seems more like an appeal to authority and intuition instead of a definite proof with formal rigorosity. Locally, there is always structure, but in pure mathematics even these steps require such an in depth understanding that trusting experts as an outsider seems to be impossible, it could as well be magic. As a programmer, I have a quite mechanistic understanding of the world, projects like http://us.metamath.org/index.html http://us.metamath.org/index.html seem to make it much more understandable. I'm wondering, if the longest path to the theorem "2 + 2 = 4" is 150 layers deep in this system, how deep would this proof be?

StefanKarpinski 11y ago

This is one of the reasons it takes a lot of training and talent to become a mathematician. If you wonder how mathematicians can do this when programmers write such buggy programs and the two processes seem so similar, I would note that I've found that mathematicians are remarkably careful, if slow, programmers and they make mistakes at a much lower rate than most programmers. If you consider moreover that mathematics is entirely free of many of the things that make programming hard – such as any kind of mutable state, input/output or concurrency – then you can see why proof may be a more reliable process than programming. Another part of is that one spends a huge amount of time questioning and testing every single step of a proof. There's a slow back-and-forth process to proving things: 1. I think this is true – let me try to prove it. 2. I get stuck on something in the proof – let me try to construct a counterexample to the specific thing I'm currently trying to prove. 3. If I can't construct a counterexample, why? That reason itself is a proof of the point I was stuck on. And so on, back-and-forth until the whole proof is done or you've managed to find some insane, devious counterexample. So by the time you've proved something, you've looked at it from every angle and considered every possibility. Mathematicians reading a proof do something very similar, but a bit more passively – it's still a very active process where you try to poke holes in every single claim and convince yourself that you can't before moving on. But a lot of the steps will be completely obvious to a trained mathematician – it's the sequence of them that's non-obvious, but once presented in order, the arc of reasoning becomes crystal clear and irrefutable.

comex 11y ago

Huh, I thought I had read somewhere that a machine checked proof of Fermat's Last Theorem had already been created. I must have mixed it up with something else.

GFK_of_xmaspast 11y ago
Are you thinking of Fermat's Little Theorem?