Hacker News Reader

Comment by kryptiskt | Hacker News Reader

One notable thing here is that the proof is a Coq proof. I wonder if it is the first significant proof that starts out implemented in a theorem prover, instead of being a known proof translated to such a system.

Note that there have been computer-assisted proofs before (four-color theorem, Kepler's conjecture), but those were not done in a formally verified setting until later.

View on HN

As far as I am aware, all of the proofs and techniques for each machine were present before mxdys managed to get the whole theorem into Coq: the main problem was that the deciders and manual proofs were disorganized and somewhat suspect. The worst offenders here were Skelet #1, which needed a bespoke program to accelerate it to its ultimate pattern [0], and Skelet #17, which took Xu seven pages' worth of dense reasoning to prove non-halting [1]. The full Coq proof put a much-needed degree of confidence into these results.

[0] https://www.sligocki.com/2023/03/13/skelet-1-infinite.html

[1] https://discuss.bbchallenge.org/t/skelet-17-does-not-halt/18...

Apparently, this is the proof in 19,000 lines of Coq: https://github.com/ccz181078/Coq-BB5/blob/main/BB52Theorem.v

> [The four color theorem] was the first major theorem to be proved using a computer.

https://en.m.wikipedia.org/wiki/Four_color_theorem

I guess maybe I don't understand what you mean by "formally verified setting", but I believe the four color theorem was first proven using a computer.

> Although flawed, Kempe's original purported proof of the four color theorem provided some of the basic tools later used to prove it.

It sounds like Kempe laid some of the groundwork, but then the theorem was ultimately proved using a computer.

I could be wrong though, I'm not an expert in this area.

The original four color theorem proof used a computer as a computational aid for some nasty casework: the procedure for checking each case and the list of cases that needed to be checked were found by hand.

Proving something in a theorem prover means the proof itself is an object constructed in the prover's language.

I think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq? Every mathematician will have plenty of hand written sketches, ideas and parts of proofs. Does that mean it was "ported" to Coq?

> I think that's a bit too harsh. An entire complicated proof concocted solely looking at a computer screen in Coq?

Nobody is suggesting this, and in this case, it was indeed "ported" to Coq from existing sketches.

The distinction here isn't between on-paper-first vs computer-first. The distinction here is between using a custom computer program to perform computations for a mostly-paper proof, versus taking an existing general-purpose theorem-checker (Coq, in this case) and writing down the entire proof in its language so it can check it.

No, the point is that the proof itself should be written in the Coq language. The original 4-color proof in 1976 was written in English. They used computer programs to do certain computations, but the proof that those programs were correct and that they were computing the right thing was written in English and checked by humans.

I'm no expert either, but it's interesting to note that the original computer-aided proof was erroneous. ctrl-f for Schmidt on the Wikipedia page.

Attempts to prove BB(5) would have begun long before theorem provers were around. This BB was discovered in 1990, and all machines of size 5 would have been enumerated not long after.

Enumerating machines is trivial. Understanding and analyzing their behavior is hard.

Reply on news.ycombinator.com