Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Flyspeck completed!

Email Gateway (Aug 19 2022 at 15:24):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Nov 21 2024 at 12:39 UTC