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. It doesn’t take an expert to state this.

Properly explain is an enormous grey area. Soon, I think, there will be proofs of results that are verified in Lean that are so long that no one will be able to “properly explain”. I don’t think they should be discarded.

Resolution of singularities is a famous theorem of Hironaka. Abhyankar claimed that no one truly understood the proof of the theorem. He said that he and Zariski couldn’t get through the paper with a full understanding. But everyone accepts this theorem as being correct.

▲

akk0 2 hours ago | parent | next [-]

For an exhaustive search, if you can explain to me: - how to exhaustively list the cases that need to be checked, and why that method is exhaustive - how to check each case, and why that works and then conclude with "we've had a computer do this exhaustive search, and the result came up as X", for me that satisfies completely understanding the proof.

▲

aleph_minus_one 2 hours ago | parent | prev | next [-]

> 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

▲

ChadNauseam 4 hours ago | parent | prev | next [-]

> One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases. It doesn’t take an expert to state this.

Hmm, doesn't it take an expert to explain why those cases are exhaustive, and why the code that checked them is correct?

Tangentially, I'm not a mathematician but I wonder if one "opaque" proof that is too complicated for anyone to understand, but that we know is correct via formal verification, might end up being built on with "transparent" human-understandable proofs. For example, it's my understanding that there are many conjectures that have been proven true conditional on the riemann hypothesis being true. In that case, an opaque proof of the riemann hypothesis would enable those conjectures to be known and built upon

	▲	czgov 3 hours ago \| parent [-]
		That will certainly happen. Humans will extend AI generated results. But what will also happen is that AI can “think” much longer than a human can and can have a vastly greater base “knowledge” than humans can have and so there will be a bewildering amount of new results. Humans may not be able to keep up. To your first point. There a large number of cases that maps can be reduced to. Very few people have checked these reductions themselves. In 50 years there will be no human alive that will have checked the reductions by hand. Do we then discard the theorem? More importantly, do we trust the people that claim to have checked all the reductions? There are hundreds of cases. I trust a computer verification much more than I’d trust human verification. Humans will likely make mistakes due to the tedium. And some will claim understanding of all cases but be wrong in their understanding in some of the cases.

▲

intuitionist 3 hours ago | parent | prev | next [-]

Nowadays the proof of resolution of singularities in characteristic zero is considered something you can teach in an intro algebraic geometry course, though. The concepts have been absorbed and are now much better understood. 4CT is very different because so much of it is exhaustive case analysis; you can understand the high-level ideas of the proof as a bright undergraduate, but you still can’t check the cases by hand

▲

4 hours ago | parent | prev [-]

[deleted]