First stated by Johannes Kepler in 1611 while investigating why snowflakes are six cornered, the conjecture concerns the most efficient way to stack identical spheres, the everyday problem of how a greengrocer stacks oranges. It stood unproved for nearly four centuries and was finally settled by a proof that was itself controversial for how it was produced: by exhaustive computer calculation rather than by hand. This description is adapted from Wikipedia contributors under CC BY-SA 4.0; changes were made. https://creativecommons.org/licenses/by-sa/4.0/
Facts
StatementNo arrangement of equally sized spheres filling space has a greater average density than the cubic close packing and hexagonal close packing arrangements, both of which fill about seventy four percent of space. 1 Classification
Statement Form FAQs
Why was a formal computer proof needed after Hales had already proved the Kepler conjecture?
The proof was too large and computer-heavy to check by hand, so the Flyspeck project formalized it, finishing in 2014.
Hales' proof was hard to check. It appears in a series of papers totaling more than 250 pages, it relies extensively on methods from global optimization, linear programming and interval arithmetic, and the computer files holding its code and data need more than 3 gigabytes of storage. Because of these difficulties in verifying it, Hales launched the Flyspeck project, short for Formal Proof of Kepler, in January 2003 to have computers check every step of the proof. The project was officially completed on August 10, 2014, using HOL Light and Isabelle to cover both the mathematical text and the computer calculations.
Connections
Associated With
Sphere Packing, Concepts The Kepler conjecture states the densest possible arrangement of non-overlapping spheres is the familiar cubic and hexagonal close packings, so its subject is the sphere packing concept itself.
Additional Source Sphere Packing (Wikipedia)Lead section
Has Statement Form
In Branch
Additional Source Kepler Conjecture (Wikipedia)Introduction
Source Kepler Conjecture (Wikipedia)
Posed By
Kepler first stated the conjecture in 1611; it was proved by Thomas Hales in 1998.
Source Kepler Conjecture (Wikipedia)
Proved By
Hales announced a proof in 1998; the Flyspeck project completed a formal machine-verified proof in 2014, accepted for publication in 2017.
Source Kepler Conjecture (Wikipedia)
Sources
1. Kepler Conjecture (Wikipedia)
Wikimedia FoundationBackground section
no arrangement of equally sized spheres filling space has a greater average density than that of the cubic close packing (face-centered cubic) and hexagonal close packing arrangements.
Origins section
The conjecture was first stated by Johannes Kepler (1611) in his paper 'On the six-cornered snowflake'.
Lead section
In 1998, the American mathematician Thomas Hales, following an approach suggested by Fejes Tóth (1953), announced that he had a proof of the Kepler conjecture.
A formal proof subsection
In 2014, the Flyspeck project team, headed by Hales, announced the completion of a formal proof of the Kepler conjecture using a combination of the Isabelle and HOL Light proof assistants. In 2017, the formal proof was accepted by the journal Forum of Mathematics, Pi.
- In Branch: Geometry
In Branch: Discrete Geometry, Introduction
is a mathematical theorem about sphere packing in three-dimensional Euclidean space.
View the Source Sphere Packing (Wikipedia)
Wikimedia FoundationAssociated With: Sphere Packing, Lead sectionQuote, Associated With: Sphere Packing, Lead section
a sphere packing is an arrangement of non-overlapping spheres within a containing space
Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.