Editing Kepler conjecture (section)

===A formal proof===
In January 2003, Hales announced the start of a collaborative project to produce a complete formal proof of the Kepler conjecture. The aim was to remove any remaining uncertainty about the validity of the proof by creating a formal proof that can be verified by [[automated proof checking]] software such as [[HOL Light]] and [[Isabelle (proof assistant)|Isabelle]]. This project was called ''Flyspeck'' – an expansion of the acronym FPK standing for ''Formal Proof of Kepler''. At the start of this project, in 2007, Hales estimated that producing a complete formal proof would take around 20 years of work.<ref>{{cite magazine|url=https://pittsburghquarterly.com/articles/thomas-hales-the-proof-of-the-proof/|magazine=Pittsburgh Quarterly|first=Jennifer|last=Bails|title=Thomas Hales: The Proof of the Proof|date=Fall 2007}}</ref> Hales published a "blueprint" for the formal proof in 2012;<ref>{{cite book | last1=Hales | first1=Thomas C. | title=Dense Sphere Packings: A Blueprint for Formal Proofs | series=London Mathematical Society Lecture Note Series | volume=400 | publisher=Cambridge University Press | isbn=978-0-521-61770-3 | year=2012}}</ref> the completion of the project was announced on August 10, 2014.<ref>{{cite web |url=https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion |title=Project Flyspeck |work=[[Google Code]]}}</ref> In January 2015 Hales and 21 collaborators posted a paper titled "A formal proof of the Kepler conjecture" on the [[arXiv]], claiming to have proved the conjecture.<ref>{{cite arXiv |eprint=1501.02155 |class=math.MG |title=A Formal Proof of the Kepler Conjecture |last=Hales |first=Thomas |author-link=Thomas Callister Hales |display-authors=etal |date=9 January 2015 }}</ref>  In 2017, the formal proof was accepted by the journal ''[[Forum of Mathematics]]''.<ref name="formalproof" />