Kepler conjecture

Last updated

The Kepler conjecture, named after the 17th-century mathematician and astronomer Johannes Kepler, is a mathematical theorem about sphere packing in three-dimensional Euclidean space. It states that 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. The density of these arrangements is around 74.05%.

Contents

In 1998, Thomas Hales, following an approach suggested by Fejes Tóth (1953), announced that he had a proof of the Kepler conjecture. Hales' proof is a proof by exhaustion involving the checking of many individual cases using complex computer calculations. Referees said that they were "99% certain" of the correctness of Hales' proof, and the Kepler conjecture was accepted as a theorem. 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 . [1]

Background

Diagrams of cubic close packing (left) and hexagonal close packing (right). Closepacking.svg
Diagrams of cubic close packing (left) and hexagonal close packing (right).

Imagine filling a large container with small equal-sized spheres: Say a porcelain gallon jug with identical marbles. The "density" of the arrangement is equal to the total volume of all the marbles, divided by the volume of the jug. To maximize the number of marbles in the jug means to create an arrangement of marbles stacked between the sides and bottom of the jug, that has the highest possible density, so that the marbles are packed together as closely as possible.

Experiment shows that dropping the marbles in randomly, with no effort to arrange them tightly, will achieve a density of around 65%. [2] However, a higher density can be achieved by carefully arranging the marbles as follows:

  1. For the first layer of marbles, arrange them in a hexagonal lattice (the honeycomb pattern)
  2. Put the next layer of marbles in the lowest lying gaps you can find above and between the marbles in the first layer, regardless of pattern
  3. Continue with the same procedure of filling in the lowest gaps in the prior layer, for the third and remaining layers, until the marbles reach the top edge of the jug.

At each step there are at least two choices of how to place the next layer, so this otherwise unplanned method of stacking the spheres creates an uncountably infinite number of equally dense packings. The best known of these are called cubic close packing and hexagonal close packing. Each of these arrangements has an average density of

The Kepler conjecture says that this is the best that can be done – no other arrangement of marbles has a higher average density: Despite there being astoundingly many different arrangements possible that follow the same procedure as steps 1–3, no packing (according to the procedure or not) can possibly fit more marbles into the same jug.

Origins

One of the diagrams from Strena Seu de Nive Sexangula, illustrating the Kepler conjecture Kepler conjecture 2.jpg
One of the diagrams from Strena Seu de Nive Sexangula, illustrating the Kepler conjecture

The conjecture was first stated by JohannesKepler  ( 1611 ) in his paper 'On the six-cornered snowflake'. He had started to study arrangements of spheres as a result of his correspondence with the English mathematician and astronomer Thomas Harriot in 1606. Harriot was a friend and assistant of Sir Walter Raleigh, who had asked Harriot to find formulas for counting stacked cannonballs, an assignment which in turn led Raleigh's mathematician acquaintance into wondering about what the best way to stack cannonballs was. [3] Harriot published a study of various stacking patterns in 1591, and went on to develop an early version of atomic theory.

Nineteenth century

Kepler did not have a proof of the conjecture, and the next step was taken by Carl FriedrichGauss  ( 1831 ), who proved that the Kepler conjecture is true if the spheres have to be arranged in a regular lattice.

This meant that any packing arrangement that disproved the Kepler conjecture would have to be an irregular one. But eliminating all possible irregular arrangements is very difficult, and this is what made the Kepler conjecture so hard to prove. In fact, there are irregular arrangements that are denser than the cubic close packing arrangement over a small enough volume, but any attempt to extend these arrangements to fill a larger volume is now known to always reduce their density.

After Gauss, no further progress was made towards proving the Kepler conjecture in the nineteenth century. In 1900 David Hilbert included it in his list of twenty three unsolved problems of mathematics —it forms part of Hilbert's eighteenth problem.

Twentieth century

The next step toward a solution was taken by László Fejes Tóth. Fejes Tóth (1953) showed that the problem of determining the maximum density of all arrangements (regular and irregular) could be reduced to a finite (but very large) number of calculations. This meant that a proof by exhaustion was, in principle, possible. As Fejes Tóth realised, a fast enough computer could turn this theoretical result into a practical approach to the problem.

Meanwhile, attempts were made to find an upper bound for the maximum density of any possible arrangement of spheres. English mathematician Claude Ambrose Rogers (see Rogers (1958)) established an upper bound value of about 78%, and subsequent efforts by other mathematicians reduced this value slightly, but this was still much larger than the cubic close packing density of about 74%.

In 1990, Wu-Yi Hsiang claimed to have proven the Kepler conjecture. The proof was praised by Encyclopædia Britannica and Science and Hsiang was also honored at joint meetings of AMS-MAA. [4] Wu-YiHsiang ( 1993 , 2001 ) claimed to prove the Kepler conjecture using geometric methods. However Gábor Fejes Tóth (the son of László Fejes Tóth) stated in his review of the paper "As far as details are concerned, my opinion is that many of the key statements have no acceptable proofs." Hales (1994) gave a detailed criticism of Hsiang's work, to which Hsiang (1995) responded. The current consensus is that Hsiang's proof is incomplete. [5]

Hales' proof

Following the approach suggested [6] by László Fejes Tóth, 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 gigabytes 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.

Hales (2005) published a 100-page paper describing the non-computer part of his proof in detail. Hales & Ferguson (2006) and several subsequent papers described the computational portions. Hales and Ferguson received the 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. 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. [7] Hales published a "blueprint" for the formal proof in 2012; [8] the completion of the project was announced on August 10, 2014. [9] 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. [10] In 2017, the formal proof was accepted by the journal Forum of Mathematics . [1]

Thue's theorem
The regular hexagonal packing is the densest circle packing in the plane (1890). The density is π⁄√12.
The 2-dimensional analog of the Kepler conjecture; the proof is elementary. Henk and Ziegler attribute this result to Lagrange, in 1773 (see references, pag. 770).
A simple proof by Chau and Chung from 2010 uses the Delaunay triangulation for the set of points that are centers of circles in a saturated circle packing. [11]
The hexagonal honeycomb conjecture
The most efficient partition of the plane into equal areas is the regular hexagonal tiling. [12]
Related to Thue's theorem.
Dodecahedral conjecture
The volume of the Voronoi polyhedron of a sphere in a packing of equal spheres is at least the volume of a regular dodecahedron with inradius 1. McLaughlin's proof, [13] for which he received the 1999 Morgan Prize.
A related problem, whose proof uses similar techniques to Hales' proof of the Kepler conjecture. Conjecture by L. Fejes Tóth in the 1950s.
The Kelvin problem
What is the most efficient foam in 3 dimensions? This was conjectured to be solved by the Kelvin structure, and this was widely believed for over 100 years, until disproved in 1993 by the discovery of the Weaire–Phelan structure. The surprising discovery of the Weaire–Phelan structure and disproof of the Kelvin conjecture is one reason for the caution in accepting Hales' proof of the Kepler conjecture.
Sphere packing in higher dimensions
In 2016, Maryna Viazovska announced proof of the optimal sphere packing in dimension 8, which quickly led to a solution in dimension 24. [14] However, the optimal sphere packing question in dimensions other than 1, 2, 3, 8, and 24 is still open.
Ulam's packing conjecture
It is unknown whether there is a convex solid whose optimal packing density is lower than that of the sphere.

Related Research Articles

<span class="mw-page-title-main">Packing problems</span> Problems which attempt to find the most efficient way to pack objects into containers

Packing problems are a class of optimization problems in mathematics that involve attempting to pack objects together into containers. The goal is to either pack a single container as densely as possible or pack all objects using as few containers as possible. Many of these problems can be related to real-life packaging, storage and transportation issues. Each packing problem has a dual covering problem, which asks how many of the same objects are required to completely cover every region of the container, where objects are allowed to overlap.

<span class="mw-page-title-main">Sphere packing</span> Geometrical structure

In geometry, a sphere packing is an arrangement of non-overlapping spheres within a containing space. The spheres considered are usually all of identical size, and the space is usually three-dimensional Euclidean space. However, sphere packing problems can be generalised to consider unequal spheres, spaces of other dimensions or to non-Euclidean spaces such as hyperbolic space.

<span class="mw-page-title-main">Discrete geometry</span> Branch of geometry that studies combinatorial properties and constructive methods

Discrete geometry and combinatorial geometry are branches of geometry that study combinatorial properties and constructive methods of discrete geometric objects. Most questions in discrete geometry involve finite or discrete sets of basic geometric objects, such as points, lines, planes, circles, spheres, polygons, and so forth. The subject focuses on the combinatorial properties of these objects, such as how they intersect one another, or how they may be arranged to cover a larger object.

<span class="mw-page-title-main">Close-packing of equal spheres</span> Dense arrangement of congruent spheres in an infinite, regular arrangement

In geometry, close-packing of equal spheres is a dense arrangement of congruent spheres in an infinite, regular arrangement. Carl Friedrich Gauss proved that the highest average density – that is, the greatest fraction of space occupied by spheres – that can be achieved by a lattice packing is

The Fulkerson Prize for outstanding papers in the area of discrete mathematics is sponsored jointly by the Mathematical Optimization Society (MOS) and the American Mathematical Society (AMS). Up to three awards of $1,500 each are presented at each (triennial) International Symposium of the MOS. Originally, the prizes were paid out of a memorial fund administered by the AMS that was established by friends of the late Delbert Ray Fulkerson to encourage mathematical excellence in the fields of research exemplified by his work. The prizes are now funded by an endowment administered by MPS.

<span class="mw-page-title-main">Rhombic enneacontahedron</span> Convex polyhedron with 90 rhombic faces

In geometry, a rhombic enneacontahedron is a polyhedron composed of 90 rhombic faces; with three, five, or six rhombi meeting at each vertex. It has 60 broad rhombi and 30 slim. The rhombic enneacontahedron is a zonohedron with a superficial resemblance to the rhombic triacontahedron.

Hilbert's eighteenth problem is one of the 23 Hilbert problems set out in a celebrated list compiled in 1900 by mathematician David Hilbert. It asks three separate questions about lattices and sphere packing in Euclidean space.

<span class="mw-page-title-main">Thomas Callister Hales</span> American mathematician

Thomas Callister Hales is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification. In representation theory he is known for his work on the Langlands program and the proof of the fundamental lemma over the group Sp(4). In discrete geometry, he settled the Kepler conjecture on the density of sphere packings and the honeycomb conjecture. In 2014, he announced the completion of the Flyspeck Project, which formally verified the correctness of his proof of the Kepler conjecture.

László Fejes Tóth was a Hungarian mathematician who specialized in geometry. He proved that a lattice pattern is the most efficient way to pack centrally symmetric convex sets on the Euclidean plane. He also investigated the sphere packing problem. He was the first to show, in 1953, that proof of the Kepler conjecture can be reduced to a finite case analysis and, later, that the problem might be solved using a computer.

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.

<span class="mw-page-title-main">Trapezo-rhombic dodecahedron</span> Polyhedron with 6 rhombic and 6 trapezoidal faces

In geometry, the trapezo-rhombic dodecahedron or rhombo-trapezoidal dodecahedron is a convex dodecahedron with 6 rhombic and 6 trapezoidal faces. It has D3h symmetry. A concave form can be constructed with an identical net, seen as excavating trigonal trapezohedra from the top and bottom. It is also called the trapezoidal dodecahedron.

<span class="mw-page-title-main">Honeycomb conjecture</span>

The honeycomb conjecture states that a regular hexagonal grid or honeycomb has the least total perimeter of any subdivision of the plane into regions of equal area. The conjecture was proven in 1999 by mathematician Thomas C. Hales.

The dodecahedral conjecture in geometry is intimately related to sphere packing.

<span class="mw-page-title-main">Circle packing</span> Field of geometry closely arranging circles on a plane

In geometry, circle packing is the study of the arrangement of circles on a given surface such that no overlapping occurs and so that no circle can be enlarged without creating an overlap. The associated packing density, η, of an arrangement is the proportion of the surface covered by the circles. Generalisations can be made to higher dimensions – this is called sphere packing, which usually deals only with identical spheres.

<span class="mw-page-title-main">Smoothed octagon</span>

The smoothed octagon is a region in the plane found by Karl Reinhardt in 1934 and conjectured by him to have the lowest maximum packing density of the plane of all centrally symmetric convex shapes. It was also independently discovered by Kurt Mahler in 1947. It is constructed by replacing the corners of a regular octagon with a section of a hyperbola that is tangent to the two sides adjacent to the corner and asymptotic to the sides adjacent to these.

<span class="mw-page-title-main">Károly Bezdek</span> Hungarian-Canadian mathematician

Károly Bezdek is a Hungarian-Canadian mathematician. He is a professor as well as a Canada Research Chair of mathematics and the director of the Centre for Computational and Discrete Geometry at the University of Calgary in Calgary, Alberta, Canada. Also he is a professor of mathematics at the University of Pannonia in Veszprém, Hungary. His main research interests are in geometry in particular, in combinatorial, computational, convex, and discrete geometry. He has authored 3 books and more than 130 research papers. He is a founding Editor-in-Chief of the e-journal Contributions to Discrete Mathematics (CDM).

<span class="mw-page-title-main">Ulam's packing conjecture</span>

Ulam's packing conjecture, named for Stanislaw Ulam, is a conjecture about the highest possible packing density of identical convex solids in three-dimensional Euclidean space. The conjecture says that the optimal density for packing congruent spheres is smaller than that for any other convex body. That is, according to the conjecture, the ball is the convex solid which forces the largest fraction of space to remain empty in its optimal packing structure. This conjecture is therefore related to the Kepler conjecture about sphere packing. Since the solution to the Kepler conjecture establishes that identical balls must leave ≈25.95% of the space empty, Ulam's conjecture is equivalent to the statement that no other convex solid forces that much space to be left empty.

In mathematics, the theory of finite sphere packing concerns the question of how a finite number of equally-sized spheres can be most efficiently packed. The question of packing finitely many spheres has only been investigated in detail in recent decades, with much of the groundwork being laid by László Fejes Tóth.

References

  1. 1 2 Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland (29 May 2017). "A Formal Proof of the Kepler Conjecture". Forum of Mathematics, Pi. 5: e2. doi: 10.1017/fmp.2017.1 . hdl: 2066/176365 .
  2. ↑ Li, Shuixiang; Zhao, Liang; Liu, Yuewu (April 2008). "Computer simulation of random sphere packing in an arbitrarily shaped container". Computers, Materials and Continua. 7: 109–118.
  3. ↑ Leutwyler, Kristin (1998-09-14). "Stack 'em Tight". Scientific American. Retrieved 2021-11-15.
  4. ↑ Hales, Thomas C. (June 1994). "The Status of the Kepler Conjecture". The Mathematical Intelligencer . 16 (3): 47–58. doi:10.1007/BF03024356. S2CID   123375854.
  5. ↑ Singh, Simon (1997). Fermat's Last Theorem . New York: Walker. ISBN   978-0-80271-331-5.
  6. ↑ Fejes Tóth 1953, p. 238.
  7. ↑ Bails, Jennifer (Fall 2007). "Thomas Hales: The Proof of the Proof". Pittsburgh Quarterly.
  8. ↑ Hales, Thomas C. (2012). Dense Sphere Packings: A Blueprint for Formal Proofs. London Mathematical Society Lecture Note Series. Vol. 400. Cambridge University Press. ISBN   978-0-521-61770-3.
  9. ↑ "Project Flyspeck". Google Code .
  10. ↑ Hales, Thomas; et al. (9 January 2015). "A Formal Proof of the Kepler Conjecture". arXiv: 1501.02155 [math.MG].
  11. ↑ Chang, Hai-Chau; Wang, Lih-Chung (22 September 2010). "A Simple Proof of Thue's Theorem on Circle Packing". arXiv: 1009.4322 [math.MG].
  12. ↑ Hales, Thomas C. (20 May 2002). "The Honeycomb Conjecture". Discrete & Computational Geometry . 25: 1–22. arXiv: math/9906042 . doi:10.1007/s004540010071. S2CID   14849112.
  13. ↑ Hales, Thomas C.; McLaughlin, Sean (2010). "The Dodecahedral Conjecture". Journal of the American Mathematical Society . 23 (2): 299–344. arXiv: math.MG/9811079 . Bibcode:2010JAMS...23..299H. doi:10.1090/S0894-0347-09-00647-X.
  14. ↑ Klarreich, Erica (March 30, 2016), "Sphere Packing Solved in Higher Dimensions", Quanta Magazine

Publications

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.