I had mentioned that. This is true today when software developers are writing proofs and why automation is useful.

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.