> 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.
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.
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.