4 ms·
AFAIK the four color theorem was not first proved with Coq, and people consider it correct regardless of whether Coq has bugs.
by j2kun 12y ago
AFAIK the four color theorem was not first proved with Coq, and people consider it correct regardless of whether Coq has bugs.
- cheatsheet 12y agoYes, the four color theorem was proven by Appel and Haken on an IBM 370-168 at the University of Illinois in June 1976. Coq was released in May 1989.
- repsilat 12y agoI'd be surprised Appel and Haken did a formal proof on their machine -- I thought they made a conventional proof with a machine-assisted enumeration of special-cases.
- cheatsheet 12y agoMy apologies for the lack of clarity: I was following the thought path that was concerned with the validity of the four color theorem proof because of the Coq bug.