-
A formal proof of the Kepler conjecture
Authors:
Thomas Hales,
Mark Adams,
Gertrud Bauer,
Dat Tat Dang,
John Harrison,
Truong Le Hoang,
Cezary Kaliszyk,
Victor Magron,
Sean McLaughlin,
Thang Tat Nguyen,
Truong Quang Nguyen,
Tobias Nipkow,
Steven Obua,
Joseph Pleso,
Jason Rute,
Alexey Solovyev,
An Hoai Thi Ta,
Trung Nam Tran,
Diep Thi Trieu,
Josef Urban,
Ky Khac Vu,
Roland Zumkeller
Abstract:
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
△ Less
Submitted 9 January, 2015;
originally announced January 2015.
-
The Yellowstone Permutation
Authors:
David L. Applegate,
Hans Havermann,
Bob Selcoe,
Vladimir Shevelev,
N. J. A. Sloane,
Reinhard Zumkeller
Abstract:
Define a sequence of positive integers by the rule that a(n) = n for 1 <= n <= 3, and for n >= 4, a(n) is the smallest number not already in the sequence which has a common factor with a(n-2) and is relatively prime to a(n-1). We show that this is a permutation of the positive integers. The remarkable graph of this sequence consists of runs of alternating even and odd numbers, interrupted by small…
▽ More
Define a sequence of positive integers by the rule that a(n) = n for 1 <= n <= 3, and for n >= 4, a(n) is the smallest number not already in the sequence which has a common factor with a(n-2) and is relatively prime to a(n-1). We show that this is a permutation of the positive integers. The remarkable graph of this sequence consists of runs of alternating even and odd numbers, interrupted by small downward spikes followed by large upward spikes, suggesting the eruption of geysers in Yellowstone National Park. On a larger scale the points appear to lie on infinitely many distinct curves. There are several unanswered questions concerning the locations of these spikes and the equations for these curves.
△ Less
Submitted 7 March, 2015; v1 submitted 7 January, 2015;
originally announced January 2015.
-
A revision of the proof of the Kepler conjecture
Authors:
Thomas C. Hales,
John Harrison,
Sean McLaughlin,
Tobias Nipkow,
Steven Obua,
Roland Zumkeller
Abstract:
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex. The process of revision and review did not end with the publication of the proof. This article summarizes the current status of a long-term initiati…
▽ More
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex. The process of revision and review did not end with the publication of the proof. This article summarizes the current status of a long-term initiative to reorganize the original proof into a more transparent form and to provide a greater level of certification of the correctness of the computer code and other details of the proof. A final part of this article lists errata in the original proof of the Kepler conjecture.
△ Less
Submitted 2 February, 2009;
originally announced February 2009.
