> I wonder what his views on the 4 color problem are. One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases.

Just burn lots of tokens on the frontier model of your choice to let the AI find a high-level argument why the four color theorem holds. :-)

--

Seriously: since there exist quite a lot of readers on HN who are both hardcore into AI and mathematical problems: This is a challenge for you.

I am looking forward to seeing an announcement of a novel high-level argument why the four color theorem holds on the first page of HN in at most a month. :-D