4 ms·
In 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
by bollu 6y ago
In 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 !