[isabelle] Flyspeck completed!



The readers of this mailing list may be interested to learn that Tom Hales's
Flyspeck project (the formal proof of the Kepler conjecture, using mainly HOL
Light but also Isabelle/HOL) has been completed 2 days ago:

https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion

http://www.newscientist.com/article/dn26041-proof-confirmed-of-400yearold-fruitstacking-problem.html#.U-ttHEhCU19

This is a landmark achievement of Tom and his collaborators and proof of the
enormous progress in our field.

Tobias




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.