The chess analogy doesn't quite work for me. In chess, an engine's move is useful because it helps you win. In math, a proof is useful because it helps you understand something - and from that, you can build more. If a proof is incomprehensible, it's like a chess move that only works in that one specific position. Useless. The ABC conjecture is a perfect example - Mochizuki's proof might be correct, but no one can follow it, so it's basically dead. AI proofs are going to be like that, but way more of them. Tao's essay is a great starting point