Hacker News Reader

Comment by czgov | Hacker News Reader

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.

View on HN

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.

But the "computer" is magic, to you.

I could prove anything by claiming I completed a trivial-to-explain exhaustive search. The only support or refutation would be someone doing their own search. It's a very weak foundation.

We already had the ABC conjecture crisis: A theorem with a human-written proof so complex that no one besides the author can understand it. Some people claim to have refuted it. Most mathematicians are unqualified to decide.

If you prove that the theorem prover’s true and false determinations are correct—in the cases in which it can make them—then Bob’s your uncle.

> 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

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.

> 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

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

Abhyankar and others spent years trying to find an easier proof. I’m not an algebraic geometer and I don’t know the state of things now. I was under the impression that on the level of Ideals, Varieties, and Algorithms one can introduce the concept and do some calculations but not present a proof of the theorem.

But the point is that pre-AI it was already the case that famous results were published that very few could understand or digest. I think it is reasonable to expect that we will soon be at a point that Lean says a theorem is correct but no human can or will ever understand the proof.

What if Lean verifies Mochizuki’s proof of the ABC conjecture. Do we disregard it becuase no other mathematician understands the proof?

Reply on news.ycombinator.com