Skip to main content
MathOverflow

Return to Answer

Added reference to paper by Polu and Sutskever
Source Link
Timothy Chow
Timothy Chow
  • 82.6k
  • 26
  • 363
  • 587

Since you mentioned 100 years out, let me suggest that the end goal is to put ourselves out of business.

We just need to formalize enough mathematics so that AI programs will get the idea of what we're trying to do. Then they'll take over the job of doing mathematics research. We won't need to formalize any old math at that point because the AIs will rediscover everything worth rediscovering anyway.

[EDIT: For an example of some first baby steps in this direction, see Generative language modeling for automated theorem proving by Stanislas Polu and Ilya Sutskever.]

I am half joking here, but only half. I don't think that the only, or even the main, goal of formalizing is to increase the certainty of a proof from 99.9% to 99.9999999%. The main goal is to enable new approaches to doing research that don't currently exist.

For that goal, complete formalization isn't necessary, but for what it's worth, I also don't believe that "chasing our tail" will be a problem. Setting aside my pie-in-the-sky vision of putting mathematicians out of business, I think that once the tools get good enough, and the mathematical populace is sufficiently trained, new proofs will be formalized as a matter of course, just as papers are now written in $\LaTeX$ as a matter of course. As for the older papers, formalizing them will be assigned as exercises for students who are just learning the system.

Since you mentioned 100 years out, let me suggest that the end goal is to put ourselves out of business.

We just need to formalize enough mathematics so that AI programs will get the idea of what we're trying to do. Then they'll take over the job of doing mathematics research. We won't need to formalize any old math at that point because the AIs will rediscover everything worth rediscovering anyway.

I am half joking here, but only half. I don't think that the only, or even the main, goal of formalizing is to increase the certainty of a proof from 99.9% to 99.9999999%. The main goal is to enable new approaches to doing research that don't currently exist.

For that goal, complete formalization isn't necessary, but for what it's worth, I also don't believe that "chasing our tail" will be a problem. Setting aside my pie-in-the-sky vision of putting mathematicians out of business, I think that once the tools get good enough, and the mathematical populace is sufficiently trained, new proofs will be formalized as a matter of course, just as papers are now written in $\LaTeX$ as a matter of course. As for the older papers, formalizing them will be assigned as exercises for students who are just learning the system.

Since you mentioned 100 years out, let me suggest that the end goal is to put ourselves out of business.

We just need to formalize enough mathematics so that AI programs will get the idea of what we're trying to do. Then they'll take over the job of doing mathematics research. We won't need to formalize any old math at that point because the AIs will rediscover everything worth rediscovering anyway.

[EDIT: For an example of some first baby steps in this direction, see Generative language modeling for automated theorem proving by Stanislas Polu and Ilya Sutskever.]

I am half joking here, but only half. I don't think that the only, or even the main, goal of formalizing is to increase the certainty of a proof from 99.9% to 99.9999999%. The main goal is to enable new approaches to doing research that don't currently exist.

For that goal, complete formalization isn't necessary, but for what it's worth, I also don't believe that "chasing our tail" will be a problem. Setting aside my pie-in-the-sky vision of putting mathematicians out of business, I think that once the tools get good enough, and the mathematical populace is sufficiently trained, new proofs will be formalized as a matter of course, just as papers are now written in $\LaTeX$ as a matter of course. As for the older papers, formalizing them will be assigned as exercises for students who are just learning the system.

Post Made Community Wiki by Todd Trimble
Source Link
Timothy Chow
Timothy Chow
  • 82.6k
  • 26
  • 363
  • 587

Since you mentioned 100 years out, let me suggest that the end goal is to put ourselves out of business.

We just need to formalize enough mathematics so that AI programs will get the idea of what we're trying to do. Then they'll take over the job of doing mathematics research. We won't need to formalize any old math at that point because the AIs will rediscover everything worth rediscovering anyway.

I am half joking here, but only half. I don't think that the only, or even the main, goal of formalizing is to increase the certainty of a proof from 99.9% to 99.9999999%. The main goal is to enable new approaches to doing research that don't currently exist.

For that goal, complete formalization isn't necessary, but for what it's worth, I also don't believe that "chasing our tail" will be a problem. Setting aside my pie-in-the-sky vision of putting mathematicians out of business, I think that once the tools get good enough, and the mathematical populace is sufficiently trained, new proofs will be formalized as a matter of course, just as papers are now written in $\LaTeX$ as a matter of course. As for the older papers, formalizing them will be assigned as exercises for students who are just learning the system.