Comment by libraryofbabel
2 years ago
> IMHO the problem now is that the foundations of mathematics are impractical. Most mathematicians don't actually do mathematics that can be tied back to the foundational axioms.
I suppose my followup to that is, why is this a problem? Does it lead to bad mathematics? (For what definition of “bad”?) Would we be able to solve unsolved problems if we tied things back to foundations more? Mathematicians have never really done much mathematics that ties back to the foundational axioms — why change? Rigor is not really much of an end in itself - surely people do mathematics because it is useful or beautiful, or both?
Much progress has been made in mathematics by demonstrating that problems in one realm are logically equivalent to solved problems in another realm, allowing proofs from the other realm to support proofs in the first. The most obvious example is the solution to Fermat's Last Theorem by Andrew Wiles, which wended far afield through the Taniyama–Shimura conjecture involving elliptic curves and modularity.
So in theory, with a solid foundation for mathematics, and new work rigorously tied back to it, this sort of thing should be both easier and more efficient.
The real benefit is certainty.
If somebody makes a proposition and nobody is able to properly vet it, or if you just get a bunch of white heads to nod sagely and endorse it, very little prevents there existing a flaw that invalidates the whole thing which might go unnoticed for decades and ruin anything anyone tries to build atop of the result.
It's the same as security hardening in code, or checking for med interactions at the pharmacists. Or checking to make sure that the absolutely correct pill is being dispensed and not mixed up "Buttle/Tuttle" style with some other similar looking pill.
Formal rigor paved all the way from the proposition to the axioms is not 100%, nothing is 100%. But formal rigor paved over that entire distance redistributes all potential for error to the proof chain itself which is now far easier for a non-AI computer to verify, and to the strength of the axioms themselves which have had more scrutiny paid to them than any other statements in the history of mathematics.
Another important point is that you do not have to go all the way back to the axioms if someone else has already formally proved other complex statements you can rely upon instead, then you only have to pave the length of your driveway to the nearest communal road.
And you can apply it, when you do, it really works.
I think AI for mathematics will help us solve unsolved problems. There should be a virtuous cycle during its development.
1. More formalized training data makes the math AI better
2. Better math AI helps us formalize more known mathematics
But right now math AI is not very useful. It isn't at the point where ChatGPT is for programming, where the AI is really helpful for a lot of programming tasks even if it isn't superhuman yet. So the virtuous cycle hasn't started yet. But I think we will get there.