Post #2438864

@tao@mathstodon.xyz Seems like a nice problem to have: too many potential proofs, and not enough trained mathematics. It may be more comfortable for us mortals to have proofs verified by humans, but that is not always possible. For example, the famous "four colour theorem" was proved by computer, and the proof then verified by computer. But (and this may be a big "but") humans wrote and checked the computer program for the "four colour theorem", whereas AI has evolved in ways mankind cannot reasonably verify.