5 ms·
Yes, 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.
by cheatsheet 11y ago
Yes, 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 11y 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 11y 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.