Timeline for four color proof
Current License: CC BY-SA 2.5
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 5, 2010 at 18:53 | comment | added | Kevin Buzzard | @supercooldave/Grant: thanks for clearing that up! So can you or anyone confirm that all the bits of the proof compile under versions of Coq that may be different but which share the same type-checking kernel? | |
| Oct 5, 2010 at 15:41 | comment | added | Grant Olney Passmore | @Kevin: By design, one need worry only if changes were made to the (small, stable) type-checking kernel. The other machinery (which may be incompatible in various versions) can be seen as an evolving set of tools for making the construction of kernel-checkable proofs easier. | |
| Oct 5, 2010 at 15:36 | comment | added | Grant Olney Passmore | An example Coq changelog: lix.polytechnique.fr/coq/distrib/V8.3-beta0/CHANGES | |
| Oct 5, 2010 at 15:15 | comment | added | supercooldave | Different versions of Coq differ in the libraries of theories and tactics and other, often superficial, features. The core logic remains the same. | |
| Oct 5, 2010 at 15:01 | comment | added | garfield | The paper count be open.And it is said someone called Simon has solved it,do anyone know?can any some find his paper? | |
| Oct 5, 2010 at 15:01 | comment | added | Kevin Buzzard | And by pessimistic meta-induction (i.e. the fact that there may well be future versions of Coq) doesn't this mean that we shouldn't believe the parts verified with the current version? ;-) | |
| Oct 5, 2010 at 14:59 | comment | added | Kevin Buzzard | Why are there various versions of Coq? Presumably because the early versions contain bugs, which then invalidate the certificates for the earlier parts of the proof ;-) | |
| Oct 5, 2010 at 14:43 | comment | added | Grant Olney Passmore | @André: +1. This is very interesting to hear! I will ask Georges about this. If true, fixing this (or as much as is feasible in the available time-frame) might make for a nice MSc project. | |
| Oct 5, 2010 at 12:46 | comment | added | André Henriques | I've heard from my colleague Wilbert van der Kallen that the formal proof of the four colour theorem was written over a time interval that was so long, that various parts of he proof have been made to compile over various versions of Coq. The problem is that these versions of Coq are not backwards compatible! So, formally speaking there is no single computed verified proof of the four colour theorem. What there is is a collection of computed checked pieces that, together, assemble into a proof. | |
| Oct 5, 2010 at 10:44 | history | answered | Ben | CC BY-SA 2.5 |