4 ms·
> I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what ot
by soVeryTired 4y ago
> I can sit down and prove something using a tool like Isabelle, and I will be as sure of its "truth" as I can possibly be, and it really doesn't matter what other people, mathematicians or not, think about it. That's the beauty of it.
But I guess the point is that almost no-one does this. I would guess that if someone tried to formally verify every published paper out there (or even every textbook), they would uncover a large number of gaps. Very few of those gaps would be unfixable, and very few results would turn out to be incorrect, but the possibility exists.
- auggierose 4y agoNot many do this currently, that is true. But this will change. In a hundred years every mathematician will do this. I think it will reach "mainstream" much much earlier than this, probably around 2030.
- ChadNauseam 4y agoProbably 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.