3 ms·
I don't really understand why the entire known mathematics is not automatically proven yet. I think the problem is that this would be a significant amount of p
by lacker 8y ago
I don't really understand why the entire known mathematics is not automatically proven yet.
I think the problem is that this would be a significant amount of programming and data entry work, and there's no incentive for anyone to put in this work. There are many important math papers that are written at a level that is enough for a human math professor to understand, but not for a symbolic mathematics program to understand.
Since math research is generally prioritized by other math professors, and the current system of publications is optimized for math professors to read, they have no incentive to convert to a "formal language proofs are what matters" model. And there is no real financial incentive for computer programmers to implement something like this if math professors don't want it.
At the end of the day, what is the benefit of formally proving mathematical theorems via computer? If the only people consuming math proofs are other mathematicians, the only point is to check that you haven't made a mistake, which is useful but perhaps not worth much investment because the current system already does okay at catching mistakes.
If you could actually develop new mathematical research more easily with computer assistance, then I think these formal methods would be quite valuable, but I don't see how that would happen.
- mrob 8y agoFormal proofs increase trust in mathematics. E.g. Fermat's Last Theorem is supposedly true, but I can't understand the proof. I have to trust the mathematicians who say the proof is correct, and I know that in other fields (most notably with the replication crisis in psychology) people accepted things as true when they weren't. If I had a formal proof I could run it through a theorem checker and see that it was correct, and I could use multiple independent implementations of the theorem checker for more confidence. If I'm using human mathematicians as black-box theorem checkers, I don't have the option of using multiple independent implementations, because all mathematicians work with other mathematicians, so it's possible that they're just agreeing with each other's mistakes. With the software I also have the option of examining how it works, all the way down to transistor level if I want to.
- lacker 8y agoBut who is demanding this sort of increased trust in abstract mathematics? Mathematicians don't seem to be demanding it, as this sort of work/research is not in high demand for publications. Non-mathematicians don't seem to be demanding it, because this sort of mathematics doesn't yet have much application outside of mathematics.