Editing Kepler conjecture (section)

==Hales' proof==
Following the approach suggested{{sfn|Fejes Tóth|1953|p=238}} by [[László Fejes Tóth]], [[Thomas Callister Hales|Thomas Hales]], then at the [[University of Michigan]], determined that the maximum density of all arrangements could be found by minimizing a function with 150 variables. In 1992, assisted by his graduate student Samuel Ferguson, he embarked on a research program to systematically apply [[linear programming]] methods to find a lower bound on the value of this function for each one of a set of over 5,000 different configurations of spheres. If a lower bound (for the function value) could be found for every one of these configurations that was greater than the value of the function for the cubic close packing arrangement, then the Kepler conjecture would be proved. To find lower bounds for all cases involved solving about 100,000 linear programming problems.

When presenting the progress of his project in 1996, Hales said that the end was in sight, but it might take "a year or two" to complete. In August 1998 Hales announced that the proof was complete. At that stage, it consisted of 250 pages of notes and 3 [[gigabyte]]s of computer programs, data and results.

Despite the unusual nature of the proof, the editors of the ''[[Annals of Mathematics]]'' agreed to publish it, provided it was accepted by a panel of twelve referees. In 2003, after four years of work, the head of the referee's panel, Gábor Fejes Tóth, reported that the panel were "99% certain" of the correctness of the proof, but they could not certify the correctness of all of the computer calculations.

{{harvtxt|Hales|2005}} published a 100-page paper describing the non-computer part of his proof in detail.
{{harvtxt|Hales|Ferguson|2006}} and several subsequent papers described the computational portions. Hales and Ferguson received the [[Fulkerson Prize|Fulkerson Prize for outstanding papers in the area of discrete mathematics]] for 2009.

===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" />