You might get the Riemann hypothesis robo-proven and unintelligibly dense. Would mathematic professionals trust it, or would they always be putting asterisks next to proofs downstream of it ?
We put asterisks next to proofs that use the axiom of choice. If a machine comes up with proof that’s not verifiable by humans, you can very well be sure that there will be asterisks.
We put asterisks next to proofs that use the axiom of choice. If a machine comes up with proof that’s not verifiable by humans, you can very well be sure that there will be asterisks.