>>12117365I am still surprised at the lack of AI progress in automating proofs, seeking smaller lemmas and proving them, etc. There is little doubt that AI should be able to eviscerate humans in proof production in general, as well as human-readable proof production in particular. Even if the formalized proof is totally incomprehensible, there would soon develop AI that produced nearly impeccable human readable proofs, including automatically skipping steps in it's exposition considered trivial to researchers. Of course, the proofs would still have to be checked in order to be considered human knowledge, but even proofs which were impossibly large (say 2 million pages in human-readable format) could eventually be considered extremely strong evidence of the validity of the proof just by dint of it having been proven by an AI system known to have produced several major <1000 page proofs known to be correct.
There would be, at the very least, new levels of evidence for propositions. At the lowest level, there would be things like numerical verification of certain cases of conjectures; at the next level, lemmas and theorems very close to a desired theorem which would intuitively imply that the desired theorem being false would be extremely strange and anamolous; followed by increasing levels of evidence in the form of AI-derived formal proofs with varying AI system reliability. Finally, human understanding of the proof would still be considered the gold standard of mathematics.
In fact, this distinction of evidence has already happened with the proof of the Four Color theorem via computer checking, which still has a form not considered entirely human comprehensible even though it has been optimized by the coq proof assistant from it's longer, original computer proof of the 1970s. There is still the desire for a shorter proof that does not require a proof assistant to verify so many steps, and this type of mathematics will probably never go away.
