Ниже приводится реферат из MathReviews,
излагающий историю вопроса и дающий исчерпывающие ссылки.
Цитата:
Hales, Thomas C.(1-PITT-NDM)
Dense sphere packings.
A blueprint for formal proofs. London Mathematical Society Lecture Note Series, 400. Cambridge University Press, Cambridge, 2012. xiv+271 pp. ISBN: 978-0-521-61770-3
52C17 (03B35 68T15)
More links
The Kepler conjecture states that the densest sphere packing of 3-dimensional space by equal spheres is attained by the FCC (face-centered cubic) lattice packing, which has density π18√. In 2005 and 2006 T. C. Hales, together with S. P. Ferguson, published a proof of the Kepler Conjecture [T. C. Hales, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185; MR2179728 (2006g:52029); Discrete Comput. Geom. 36 (2006), no. 1, 5–20; MR2229657 (2007d:52021); T. C. Hales and S. P. Ferguson, Discrete Comput. Geom. 36 (2006), no. 1, 21–69; MR2229658 (2007d:52022); T. C. Hales, Discrete Comput. Geom. 36 (2006), no. 1, 71–110; MR2229659 (2007d:52023); Discrete Comput. Geom. 36 (2006), no. 1, 111–166; MR2229660 (2007d:52024); S. P. Ferguson, Discrete Comput. Geom. 36 (2006), no. 1, 167–204; MR2229661 (2007d:52025); T. C. Hales, Discrete Comput. Geom. 36 (2006), no. 1, 205–265; MR2229662 (2007d:52026)]. A revision to this proof made in 2010 appears in [T. C. Hales et al., Discrete Comput. Geom. 44 (2010), no. 1, 1–34; MR2639816 (2012h:52044)]. All the papers on this proof, including the revision and supporting work, are collected in the volume [T. C. Hales and S. P. Ferguson, The Kepler conjecture, Springer, New York, 2011; MR3075372].
The Kepler conjecture is an asymptotic statement about packing large volumes of space with spheres. A general approach to the Kepler Conjecture was suggested in the 1950's by L. Fejes Tóth [Lagerungen in der Ebene, auf der Kugel und im Raum, Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, Band LXV, Springer, Berlin, 1953; MR0057566 (15,248b)] via proving some type of local density inequality around each sphere center; see [J. C. Lagarias, Discrete Comput. Geom. 27 (2002), no. 2, 165–193; MR1880936 (2002k:52027)] for general background. A local density inequality is a logically stronger statement than the Kepler Conjecture because it also proves that certain local densities within a finite region of a fixed size cannot exceed the Kepler Conjecture density. The proof of Hales and Ferguson proceeds by formulating a particular local density inequality near each individual sphere in a given packing, which has the property of implying Kepler's conjecture, and which could in principle be verified by a finite computation. The inequality was very complicated, having features which would simplify the subsequent computer calculations to a point where they became feasible, and in particular giving a way to list all the possible configurations to be checked. The actual proof had many thousands of cases and intensive computer calculations.
Since 2006 Hales has engaged in a project to produce a formal proof of the Kepler Conjecture, terming the project Flyspeck. A formal proof is a proof written in a formal logical system, which can itself be verified by computer by a proof assistant that checks the proof logically line by line. Formal proofs are more reliable than proofs written in mathematics journals; the latter are like computer program specifications, while a formal proof is analogous to a computer program itself. The planned formal proof of Kepler's Conjecture is intended to be checked by computer using the proof assistant HOL light [J. R. Harrison, in Theorem proving in higher order logics, 60–66, Lecture Notes in Comput. Sci., 5674, Springer, Berlin, 2009; MR2550931]. Some statements in the formal proof will be inequalities checked by computer. Other parts require first formalizing some parts of Euclidean geometry going beyond D. Hilbert's work on foundations of geometry [Grundlagen der Geometrie, fourteenth edition, Teubner-Arch. Math. Suppl., 6, Teubner, Stuttgart, 1999; MR1732507 (2000j:01120)]. Such a formalization, which includes notions of point set topology, is described in work of Harrison [J. Automat. Reason. 50 (2013), no. 2, 173–190; MR3016800]. When completed such a formal proof will be among the largest formal proofs, comparable with the formal proof of the Feit-Thompson theorem that all odd-order finite groups are solvable, undertaken by G. Gonthier [in Interactive theorem proving, 2, Lecture Notes in Comput. Sci., 6898, Springer, Heidelberg, 2011; MR2877865].
The present book reports on part of this project. Its object is to present a blueprint version of the formal proof: a structure which will be a guide to constructing the detailed formal proof organized in a suitable way for conversion to a formal proof. The book is self-contained and does not require any knowledge of the previous proofs.
This formal proof aims to establish an entirely new set of local inequalities that imply Kepler's conjecture. It will constitute a new second-generation proof of the Kepler Conjecture logically independent of the previous proof, which proves entirely new inequalities. The new local inequalities are motivated by work of C. Marchal [Math. Z. 267 (2011), no. 3-4, 737–765; MR2776056 (2012b:52032)] which we now review. Marchal associated to a given saturated packing of spheres a partition of space into cells of four types, plus possibly some unused extra volume. (The cells are closed and overlap on volume zero sets.) The cells of type 1 are tetrahedra with vertices at 4 different sphere centers. The cells of type 2 are tetrahedra with vertices at 3 sphere centers plus one extra vertex which is strictly outside any sphere. The cells of type 3 are (roughly) unions of two truncated half-cones having 2 vertices at sphere centers. The cells of type 4 are truncated half-cones with a vertex at a sphere center (and edge length 2√). The cells of all types having a given sphere center as vertex contain within them the entire sphere.
The Marchal approach has as a main ingredient a specific choice of weight function f(h) defined for h≥0 which is compactly supported, which weights nearby volume. Associated to a sphere center v is the set of all Marchal cells having v as a vertex. These cells fill out the whole solid angle at v and each one of them will be assessed for a volume proportional to their solid angle subtended at v, using the weight function, corrected by their shape. Then to prove Kepler's conjecture two types of inequalities are required to be satisfied. The first local inequality says that the assessed volume at each sphere center will total up to at least the amount required by Kepler's conjecture. It is actually expressed in a negative form, that a certain amount of "given up'' volume is not too large, taking the form that Lf(V,v)≤12, where Lf(V,v):=∑w∈V∖vf((||w−v||)/2). The second type of local inequality says that for each Marchal cell X the total volume assessed to it by all the sphere centers at its vertices is at most the total volume of X. For type 1 and type 2 cells this inequality is expressed as γ(X,f)≥0, where γ(X,f):=vol(X)−2m1πtsol(X)+8m2π∑edih(X,e)f(∥e∥), where e is an edge and ∥e∥ its length. Here tsol(X) is the total solid angle of the sphere center vertices (up to 4π), while dih(X,e) is the dihedral angle (up to 2π), and f(⋅) is the weight function. Marchal proposed a function f(h)=M(h) which is positive up to h+=1.3254 and is zero above h=2√, and presented evidence that both types of inequalities above should hold for this function. This is Marchal's approach to the Kepler conjecture, but the details he supplies are not complete.
The new local inequalities of Hales use the Marchal partition of space into cells, together with a simpler function f(h)=L(h) which is piecewise linear, having L(h)=1 for h≤1, L(h)=0 for h≥1.26 and linearly interpolates between these values. The important point is its cutoff value 1.26 which is smaller than the 1.3254 used by Marchal and so reduces the complexity of the later analysis of counterexample configurations. A price paid for this is that the individual cell inequalities γ(X,L)≥0 for the function L(h) do not always hold. The bad cases, treated in section 6.4, concern cells having an edge of length in interval [h−,h+]≈[1.23175,1.3254], which are termed critical edges. Cells with such edges are weighted and grouped into clusters sharing a common critical edge; the weights for cells with several critical edges are arranged so that their contributions to different clusters add up to 1. The replacement for the second inequality γ(X,L)≥0 in this case is Theorem 6.93, which asserts nonnegativity for a sum of weighted γ(X,L) over a cluster, after an additional correction term is included. It requires an enormous computer calculation.
The heart of the new blueprint proof is then a proof of the first local inequality LL(V,v)=∑w∈V∖vL((∥w−v∥)/2)≤12. This part of the proof is now a finite-dimensional nonlinear optimization problem, and Hales now develops and formalizes ideas used in the earlier proof, to systematize finding and discarding a large number of cases. It shows that a counterexample local configuration can be taken to have several extra desirable properties, which he terms being a contravening configuration. By locating v=0 and letting W now be the finite set of sphere centers with ∥w∥≤2.52, these properties are: one may reduce to the case where W has cardinality 13, 14 or 15, it is a local maximum of the function LL(W,v), and the projections w/∥w∥ on the unit sphere, when connected with geodesic arcs for any two w1,w2 within distance 2.52 forms a planar graph on the surface of the sphere, with all faces being geodesic polygons having all angles less than π. The argument then classifies all such planar graphs having some extra structure, which are termed tame hypermaps. Part of the proof shows that there is a finite list of such tame hypermaps, and determines them all. To each hypermap is associated a family of linear programs to obtain upper bounds on LL(W,v). The linear programs now show for each such configuration that LL(W,v)<12, i.e. the linear program is infeasible. This can be certified by a certificate of infeasibility. and such bound may be established by suitable linear programs, concocted using many auxiliary geometric properties of such sphere center configurations W.
The book is divided into three parts. Part I of the book has one chapter, giving a historical overview of work on the problem in Sections 1.1 to 1.5, finishing in Section 1.6 with a sketch of the planned blueprint proof.
Part II, Chapters 2 to 5, gives geometric foundations for the proof. Chapter 2 treats trigonometry equalities and inequalities. Chapter 3 treats volumes. Chapter 4 treats the concept of a hypermap, which is a combinatorial structure which replaces the notion of planar map used in the original proof of the Kepler conjecture. Chapter 5 introduces a notion of "fan'' to describe hypermaps further; this notion is different from that of "fan'' in toric varieties.
Part III, Chapters 6 to 8, then presents a detailed outline of the blueprint of a new proof of the Kepler conjecture which is planned to be converted to a formal proof. Chapter 6 details the Marchal cell partition and formulates local inequalities. Chapter 7 presents main technical estimates for looseness of a packing in terms of fan parameters, given in Theorem 7.43. Chapter 8 addresses the first local inequality above. Section 8.6 uses similar ideas to present a new proof of the Dodecahedral Conjecture, done originally by Hales and S. McLaughlin [J. Amer. Math. Soc. 23 (2010), no. 2, 299–344; MR2601036 (2011d:52037)], proving a strong form that characterizes the case of equality.
Кому интересно, обращайтесь в ЛС, я могу переслать книгу
Hales, Thomas C.
Dense sphere packings.
A blueprint for formal proofs. London Mathematical Society Lecture Note Series, 400. Cambridge University Press, Cambridge, 2012. xiv+271 pp.
