We don’t need mathematicians to clear the proof as valid if it is checked by a formal proof system. Mathematicians would only need to check the theorem itself to make sure it describes what it should describe.
I think chess and go are a bad comparison. Their solving does not conclude in some societal use. They are interesting only as problems, but mathematics is interesting as a solution too.
Mathematics, and really any other subject, are not just about solving formalized problem.
It is much more important to understand what question to ask.
One of my colleague once said the definitions in a good (computer science) paper should be the most interesting part, theorem statements should be the second interesting, and the proofs should be obvious.
Formal proof means nothing if it cannot give us insight in other proofs.
Same with open problems, Mathematician love open problems because given that no expert are able to solve them, their solution likely involves novel mathematical ideas.
Fermat’s last theorem on its own is no where near as interesting as the mathematics that leads to its soluion.
Given that AI have yet to be able to wield the mathematical corpus effectively in solving large projects (or even fully autonomously improve large software), it would need human guidence, and by that, human experts are needed to understand the problem.
To qoute another one of my colleagues, people orchestrated AI to solve an open problem are simply the apple falling on Newton’s head.
Apple “knows” about the existence of gravity, because its motion follows it, but it takes a Newton to formulate and explain gravity that leads to a number of technological advancement later.
Without the question “why do apple fall”, apple will keep falling, we will keep noticing it, but we would never turn that observation into useful technologies we enjoy today.
We don’t need mathematicians to clear the proof as valid if it is checked by a formal proof system. Mathematicians would only need to check the theorem itself to make sure it describes what it should describe.
I think chess and go are a bad comparison. Their solving does not conclude in some societal use. They are interesting only as problems, but mathematics is interesting as a solution too.
Mathematics, and really any other subject, are not just about solving formalized problem. It is much more important to understand what question to ask.
One of my colleague once said the definitions in a good (computer science) paper should be the most interesting part, theorem statements should be the second interesting, and the proofs should be obvious.
Formal proof means nothing if it cannot give us insight in other proofs.
Same with open problems, Mathematician love open problems because given that no expert are able to solve them, their solution likely involves novel mathematical ideas. Fermat’s last theorem on its own is no where near as interesting as the mathematics that leads to its soluion.
Given that AI have yet to be able to wield the mathematical corpus effectively in solving large projects (or even fully autonomously improve large software), it would need human guidence, and by that, human experts are needed to understand the problem.
To qoute another one of my colleagues, people orchestrated AI to solve an open problem are simply the apple falling on Newton’s head. Apple “knows” about the existence of gravity, because its motion follows it, but it takes a Newton to formulate and explain gravity that leads to a number of technological advancement later. Without the question “why do apple fall”, apple will keep falling, we will keep noticing it, but we would never turn that observation into useful technologies we enjoy today.