@slowcoding@social.vivaldi.net @tao@mathstodon.xyz Automatic theorem provers in the past haven't been able to solve mainstream open problems. Or anyway, occasional exceptions were noteworthy and interesting, rather than the sound of an oncoming steamroller. Meanwhile here's something by @wtgowers@mathstodon.xyz referencing Doron Zeilberger saying any human-proved theorem must be "trivial": https://www.dpmms.cam.ac.uk/~wtg10/zeilberger.html