Comment by scarmig
2 hours ago
> Isn’t this a problem with human proofs as well?
Human proofs are themselves a kind of a proof of work. They certainly write flawed proofs, but you can expect a human author of a paper to have put in more effort--substantially more--than the human reader needs to verify it. Arguably, this asymmetry disappears for generated proofs.
Automated theorem provers help a bit here, but they don't eliminate the human verification cost.
That doesn’t mean it isn’t a problem for human proofs as well. Mathematicians use affiliations and c.v.’s as their primary means of gatekeeping for review, not the effort that went into a proof or its superficial appearances. Especially in hard and big problems which have had any number of flawed proofs.
Even Grigori Perelman took years to have his proof of Poicaré conjecture accepted, and he had a Ph.D. and a Berkeley fellowship.
Expecting a human author to put substantially more effort into a proof than needed to verify it is oversimplifying. It is more a matter of credentialing and collegiality in mathematics whereby someone’s reputation and work-product demonstrates that a purported proof put forward for review is likely to be true or at least a valuable or interesting contribution even if imperfect.
AI makes this a much bigger challenge.