Correctness is essential, but another highly desirable property of a mathematical proof is its insightfulness, that is, whether they contain interesting and novel ideas that can later be reused in others’ work (often they are regarded as more important than a theorem itself). These others are humans and they desire, let’s call it, “human-style” insights. Perhaps if we had AIs that “desired” “computer-style” insights, some people (and AIs) would write their papers to provide them and investigate problems that are most likely to lead to them. Proofs that involve computers are often criticized for being uninsightful.
Proofs that involve steps that require use of computers (as opposed to formal proofs that employ proof assistants) are sometimes also criticized for not being human verifiable, because while both humans make mistakes and computer software can contain bugs, mathematicians sometimes can use their intuition and sanity checks to find the former, but not necessarily the latter.
Mathematical intuition is developed by working in an area for a long time and being exposed to various insights, heuristics, ideas (mentioned in a first paragraph). Thus not only computer based proofs are harder to verify, but also if an area relies on a lot of non human verifiable proofs that means it might be significantly harder to develop an intuition in that area which might then make it harder for humans to create new mathematical ideas. It is probably easier understand the landscape of ideas that were created to be human understandable.
That is neither to say that computers have little place in mathematics (they do, they can be used for formal proofs, generating conjectures or gathering evidence for what approach to use to solve a problem), nor it is to say that computers will never make human mathematicians obsolete (perhaps they will become so good that humans will no longer be able to compete).
However, it should be noted that some people have different opinions.
Automated theorem proving is a different problem entirely and it’s obviously not ready yet to take the place of human mathematicians. I’m not in disagreement with you here.
However there’s no conflict between being ‘insightful’ and ‘intuitive’ and being computer-verifiable. In the ideal case you would have a language for expressing mathematics that mapped well to human intuition. I can’t think of any reason this couldn’t be done. But that’s not even necessary—you could simply write human-understandable versions of your proofs along with machine-verifiable versions, both proving the same statements.
Correctness is essential, but another highly desirable property of a mathematical proof is its insightfulness, that is, whether they contain interesting and novel ideas that can later be reused in others’ work (often they are regarded as more important than a theorem itself). These others are humans and they desire, let’s call it, “human-style” insights. Perhaps if we had AIs that “desired” “computer-style” insights, some people (and AIs) would write their papers to provide them and investigate problems that are most likely to lead to them. Proofs that involve computers are often criticized for being uninsightful.
Proofs that involve steps that require use of computers (as opposed to formal proofs that employ proof assistants) are sometimes also criticized for not being human verifiable, because while both humans make mistakes and computer software can contain bugs, mathematicians sometimes can use their intuition and sanity checks to find the former, but not necessarily the latter.
Mathematical intuition is developed by working in an area for a long time and being exposed to various insights, heuristics, ideas (mentioned in a first paragraph). Thus not only computer based proofs are harder to verify, but also if an area relies on a lot of non human verifiable proofs that means it might be significantly harder to develop an intuition in that area which might then make it harder for humans to create new mathematical ideas. It is probably easier understand the landscape of ideas that were created to be human understandable.
That is neither to say that computers have little place in mathematics (they do, they can be used for formal proofs, generating conjectures or gathering evidence for what approach to use to solve a problem), nor it is to say that computers will never make human mathematicians obsolete (perhaps they will become so good that humans will no longer be able to compete).
However, it should be noted that some people have different opinions.
Automated theorem proving is a different problem entirely and it’s obviously not ready yet to take the place of human mathematicians. I’m not in disagreement with you here.
However there’s no conflict between being ‘insightful’ and ‘intuitive’ and being computer-verifiable. In the ideal case you would have a language for expressing mathematics that mapped well to human intuition. I can’t think of any reason this couldn’t be done. But that’s not even necessary—you could simply write human-understandable versions of your proofs along with machine-verifiable versions, both proving the same statements.