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.