3 ms·
Probably by 2030 and by 2040 at the latest, you will be able to give a proposition to a machine learning model and the model will output a machine-verifiable pr
by ChadNauseam 4y ago
Probably by 2030 and by 2040 at the latest, you will be able to give a proposition to a machine learning model and the model will output a machine-verifiable proof of its truth or falsity at least as often as a human can.
- auggierose 4y agoIt's not that easy. Humans often work weeks, months, or even years towards proving a theorem. They need to build new theories for it, generalise the theorem, etc., before the proof becomes possible. I would not expect machines to be able to prove any of those theorems by 2030 automatically without human guidance (but maybe I am too pessimistic!) I definitely would expect machines to be able to do the sort of effortless small step reasoning that humans are capable of, and that's really all that is needed for proof assistants to go main stream. It is already possible to a certain extent now, but it needs to get a whole lot better.