It better not have 100s of individually checked configurations
Edit: damn it.
I was just thinking last night about the four color theorem in the context of the recent Navier-Stokes drama, and Tao's Mastodon post on the uselessness of inscrutable computer-generated formalizations. I would love for an AI company find a proof of the four-color theorem without individually checked configurations, and optimize it for human comprehensibility.
Edit: damn it.
I was just thinking last night about the four color theorem in the context of the recent Navier-Stokes drama, and Tao's Mastodon post on the uselessness of inscrutable computer-generated formalizations. I would love for an AI company find a proof of the four-color theorem without individually checked configurations, and optimize it for human comprehensibility.