One of the on-going arguments in automated theorem proving has been this central question: would anyone understand or want to read a proof written by a machine?
A big part of why we write them and enjoy them is elegance, a rather subjective quality appreciated by people.
In computer science we don't tend to care so much for this quality; if the checker says the proof is good that's generally about as far as we take it.
But endearing proofs that last? That people want to read? That's much harder to do.
You would still need to be able to read the proof that a computer generated and understand what it contains in order to judge whether it is correct with respect to your specifications. So in some sense elegance would be useful since the proof isn’t written by a human but has to be understood by one.
If the input here is still plain language prompts… then we’ll have to assume that we eventually develop artificial cognition. As far as I know, there isn’t a serious academic attempting this, only VC’s with shovels to sell.
https://deepmind.google/discover/blog/alphageometry-an-olymp...
At least in principle. Practically, any system as least as powerful as first-order logic is undecidable, so there can never be any computer program that would be able to do this perfectly. It might be that some day, an AI could be just as good as a trained mathematician, but so far, it doesn't look like it.