3 ms·
I'm no mathematician but let's imagine you approach is followed. Computers do prove (or disprove) a lot of the open question (theorems we have no proof for). So
by wiz21c 6y ago
I'm no mathematician but let's imagine you approach is followed. Computers do prove (or disprove) a lot of the open question (theorems we have no proof for). So far so good, the current math is "solved". But now, you have to make new math, discover/create new theorems. If you leave it to the computers, they'll generate millions of truth. But who will be able to understand and value those truths ? If you either leave it to humans, they'll first have to understand all the theorems proven above in order to be able to formulate new theorems. They'll have to deeply understand them, to abstract them to be able to use them as a foundation for new work.
So my impression is that sooner or later, humans reenter the loop. However, if a computer proves that a new theorem is true, say with an impossible to understand proof then it means that's it's worth investing human time in that proof.
So it'd be helpful.
- bollu 6y agoIn the above setting, we don't have computers _finding theorems_. We're using computers to _machine check_ our proofs; The process of verifying whether a proof is correct or not is mechanical when a proof is broken down to its smallest steps. The proof assistant simply assists us in making sure we haven't missed anything. If you are interested in humans and machines working together to find proofs, then boy do I have a story for you: http://math.iisc.ac.in/~gadgil/presentations/SummerCSIISc.html#/ http://math.iisc.ac.in/~gadgil/presentations/SummerCSIISc.ht...
- wiz21c 6y agoThx for pointing that presentation. I must admit the maths are way beyond what I can understand. But I get the general principle of the goals. That's quite inspiring, and a little crazy too :-) Thanks a lot, that was very interesting !