Variations on five-dimensional sphere packings

Henry Cohn; Isaac Rajagopal

REVIEW 2 major objections 4 minor 1 cited by

Variations on five-dimensional sphere packings

T0 review · 2 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves there are at least four non-isometric 40-point kissing configurations in five dimensions, constructs one new one (R5), and uses the same layer-replacement idea to produce a second 306-point kissing configuration in nine…

desk verdict New 5D and 9D kissing configurations are solid and checkable, but Theorem 4.3's uniform-packing classification has a real gap: local induction doesn't exclude disconnected uniform packings. read the letter →

arxiv 2412.00937 v3 pith:SGMUIAXZ submitted 2024-12-01 math.MG math.CO

Henry Cohn , Isaac Rajagopal This is my paper · ORCID

classification math.MGmath.CO MSC 52C1711H31

keywords kissingnumberspherepackingsfivedimensionsnineuniformlayerreplacementsphericalcodesRieszenergy

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper establishes that the five-dimensional kissing problem has more geometric diversity than previously known: there are at least four non-isometric configurations of 40 points on a sphere with mutual angular separation at least $\pi/3$, one of which, R5, is new. It then shows that these configurations extend to five-dimensional sphere packings at the best known density, and that exactly six uniform packings carry these four local configurations. The same layer-replacement mechanism yields a second non-isometric 306-point kissing configuration in nine dimensions. None of the constructions improves the known density or kissing-number records; instead, they show the record values are realized by genuinely different geometries, and they expose an unusual amount of flexibility in dimension five. The paper also proposes a two-dimensional coloring framework that, if its conjecture holds, would classify every weakly recurrent optimally dense five-dimensional packing.

What carries the argument

The carrying mechanism is layer replacement: slice a known kissing configuration by a hyperplane, keep the central cross section and one outer layer, and replace the opposite layer with a reflected or coordinate-modified copy of the retained one. The admissibility of a replacement is controlled by the deep holes of the central spherical code, the points on the sphere that are as far as possible from all configuration points; a replacement layer is allowed exactly when its points nestle into those holes without violating the $\pi/3$ separation bound. For packings, the machinery is a four-coloring construction: five-dimensional packings are obtained by stacking translates of the D3 root lattice over a two-dimensional point configuration whose vertices carry colors 0,1,2,3, with distance rules for same, adjacent, and opposite colors. Valid colorings of edge-to-edge tilings by two specific triangles realize the desired kissing configurations, and a depth-first search over isometric embeddings of overlaps is used to prove uniqueness of the uniform packings. Non-isometry of configurations is certified by counting antipodal pairs and by comparing the full histogram of inner products.

What would settle it

A concrete way to test the central non-extendability claim is to search the 32 deep holes of Q5 for 16 points with pairwise inner product at most $2/5$; finding such a subset would directly refute the paper's assertion that no admissible extension exists.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that the record-achieving kissing configurations in five and nine dimensions are not unique, and that the new examples arise from a simple modification of known ones. Starting from L5, the authors replace one outer layer by the reflection of the other across the central hyperplane to get R5; the new configuration is certified as distinct by its antipodal-pair count (12, versus 20, 24, and 20 for D5, L5, and Q5). The same idea works in nine dimensions: modifying one layer of the previously known 306-point configuration produces a new configuration that has broken antipodal symmetry and fewer close pairs. For packings, the paper proves that up to isometry there are exactly six uniform five-dimensional packings whose kissing configuration is one of D5, L5, Q5, or R5; the Q5 packing is 2-periodic and the R5 packing is 4-periodic, and every symmetry of the kissing configuration extends to the packing. It also reports that Q5 and R5 cannot be extended to six dimensions by the layer method, because no admissible 16-point subset of deep holes exists, and conjectures that no six-dimensional kissing configuration with 72 or more points contains either as a cross section.

Load-bearing premise

The load-bearing assumption is that the finite depth-first computer searches are complete and correctly implemented, because the uniqueness of the uniform packings and the non-existence of six-dimensional extensions both rest on those searches.

Editorial extensions

If this is right

Any future proof or classification of optimal five-dimensional packings must accommodate four non-isometric extremal kissing configurations, not just the originally known one.
Within the family of uniform packings, the classification is complete: a uniform five-dimensional packing with any of these kissing configurations is one of six listed packings, one with D5, three with L5, one with Q5, and one with R5.
The layer method used for Q5 and R5 cannot extend them to six dimensions, so the new flexibility appears to be special to dimension five unless a different construction is found.
In nine dimensions, the new 306-point configuration achieves the same kissing record but has fewer pairs at the minimal distance and lower Riesz energy for large exponents, so energy-based selection would prefer the original configuration.
If the proposed conjecture is correct, every weakly recurrent optimally dense five-dimensional packing is represented by a valid four-coloring of a triangular tiling, turning the classification into a two-dimensional problem.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The layer-replacement trick reads as a mutation operation on spherical codes; systematically testing all admissible replacements in dimensions 5 through 9 could uncover further configurations, with the six- and seven-dimensional failures acting as constraints on when mutations exist.
The four-coloring framework converts density optimality for this family into a two-dimensional conjecture; proving that conjecture would establish optimality only among packings built this way, but it would be a concrete stepping stone toward the unsolved five-dimensional sphere packing problem.
The inner-product histograms induce an energy ordering on record configurations, suggesting that Riesz-energy minimization and kissing-number maximization favor different geometries; searches in unsolved dimensions might profit by optimizing both objectives separately.
In nine dimensions the modified layer is obtained by swapping coordinates inside the supporting binary code; since the underlying constant-weight code is unique, further geometric diversity would have to come from different sign patterns or layer choices rather than different codes.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

First, the good news: the paper's existence claims are real. R5 is a genuinely new 40-point kissing configuration in R5, distinct from D5, L5, and Q5 by antipodal-pair count and inner product spectrum. The nine-dimensional modification of Leech-Sloane is also new, and the coordinates are all in the paper and the deposited code. The five-dimensional packing construction via four-colored tilings is elegant, and the authors are properly careful about attributing the Q5 uniform packing to Andreanov-Kallus. The code deposit at DSpace is a real plus; anyone can verify the inner product counts and the search outputs.

The soft spot is Theorem 4.3, and it is not minor. The proof shows that if the kissing configuration at every point of the initial shell K0 is uniquely determined, then by induction the entire uniform packing is determined. That induction only determines the connected component of the origin. Nothing in the proof rules out a uniform packing made of two widely separated copies of the same periodic cluster, with a translation swapping the two components. If the gap is large enough, every sphere still has the same kissing configuration, so the packing is uniform. The paper does not report a search that propagates through the whole fundamental domain, nor does it give the iteration count or the size of the cell generated. Without that, 'there is at most one uniform packing' does not follow. I checked the stress-test concern against the proof text, and it holds up.

The other weakness is that the key searches are not formally verified, so the completeness claims rest on code. That is a normal situation in this kind of paper, but it makes the missing global-propagation argument more important, not less.

Bottom line: the paper is worth refereeing, and the constructions are likely correct. But Theorem 4.3 needs either a repaired proof that handles disconnected components or a more modest statement. I would not accept as-is; major revision. The reader's ACCEPT is a bit too generous on this point. Who this is for: sphere packing people, discrete geometers, coding theorists. Bring to reading group if you want to discuss what 'uniform' should mean.

Referee Report

2 major / 4 minor

Summary. The paper studies five-dimensional kissing configurations and sphere packings. It introduces a new 40-point kissing configuration R5 by modifying a layer of L5, and proves Theorem 2.1 that D5, L5, Q5, and R5 are pairwise non-isometric, using antipodal-pair counts and inner-product spectra. It then uses a four-coloring construction over D3 layers to produce sphere packings, including two new uniform packings with Q5 and R5 kissing configurations, and states Theorem 4.3 classifying uniform packings with these local configurations. In Section 5 it constructs a new 306-point nine-dimensional kissing configuration by modifying a layer of the Leech-Sloane configuration, proving Theorem 5.1. The paper deposits verification code at DSpace@MIT and positions the results as geometrically distinct constructions that match, but do not improve, known records.

Significance. If Theorem 4.3 is established, it completes the enumeration of uniform five-dimensional packings with the known extremal local kissing configurations and adds two new uniform packings to Leech's list. The new R5 and nine-dimensional configurations are explicit and machine-checkable, with full coordinate tables and inner-product counts. The constructions are parameter-free and produce falsifiable claims, and the code deposit is a genuine strength that supports the computational assertions.

major comments (2)

[§4.2, Theorem 4.3] The proof of Theorem 4.3 does not justify the step from local uniqueness of kissing configurations to uniqueness of the entire uniform packing. Uniformity, as defined in the paper (transitive automorphism group on spheres), does not imply that the tangency graph is connected; a uniform packing could a priori consist of multiple components with no contacts between them, each component carrying the same kissing configuration. The induction shows at most one connected component, not at most one packing, and the text does not report the search's stopping criterion, iteration count, or whether it generates periods/fundamental cells that would rule out further components. Please either add an explicit argument that the contact graph is connected for these kissing configurations (for example, using density or covering-radius constraints) or state Theorem 4.3 for connected uniform packings, and make any intended density assumption explicit in the theorem statement.
[§4.2, proof paragraph] The sentence 'iterating this procedure determines Kv for every v ∈ K0' is ambiguous and insufficient. If v ranges only over the initial 40-point shell, the argument determines at most the first two shells of the packing. If v ranges over newly generated points, the paper should define the growth process explicitly and prove that it exhausts all spheres of the packing; otherwise the conclusion 'there is therefore at most one uniform packing' does not follow. This is the load-bearing step for the classification claim.

minor comments (4)

[§3 and §5] The statements 'one can check by depth-first search' (Section 3) and 'one can check that there are exactly eight other triples' (Section 5) would be easier to verify if the paper stated the precise search parameters, the relevant code file in the DSpace deposit, and, where possible, a short certificate or enumeration summary.
[§4.2] The paragraph before Theorem 4.3 mentions 'with the same density as the D5 root lattice', but the theorem statement itself refers only to 'uniform sphere packings'. Please reconcile these, since the statement and proof currently appear to quantify over different classes of packings.
[§2, Table 2.2] Table 2.2 is visually dense and easy to misread; separating the four configurations with rules or explicit labels would improve clarity.
[§2, displayed coordinate lists] The notation 'permute' in displayed coordinate lists is informal; a sentence explaining that it means all permutations of the listed coordinates would help readers.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: all new constructions are explicit and verified by invariants, with prior results used only as context or external inputs.

full rationale

The paper's central claims are existence and non-isometry of explicit kissing configurations and packings. R5 is given by explicit coordinates obtained by modifying a layer of L5, and its non-isometry from D5, L5, and Q5 is established by an independent invariant: the number of antipodal pairs (12 versus 24 or 20). Theorem 2.1 therefore rests on direct construction and verification, not on any fitted parameter or assumed conclusion. The nine-dimensional configuration in Section 5 is likewise explicitly defined by swapping coordinates in a layer, and its novelty is checked by counting inner products and symmetry group orders, both of which are computed from the coordinates rather than presupposed. Theorem 4.3 is a classification statement whose proof uses a depth-first search plus an external classification by Conway and Sloane [5]; the search verifies uniqueness of extensions of local overlaps, and the conclusion is not derived from the statement being proved. The self-citations in the paper, such as [3] and [4], occur in the introduction as background on prior classifications and proved results, and they are not load-bearing for any new theorem. The paper contains no fitted parameters renamed as predictions, no ansatz smuggled in via self-citation, and no uniqueness claim imported from the authors' own prior work as the decisive step. The skeptical concern about completeness of the finite searches is a correctness or verification risk, not a circularity risk: even if a search were incomplete, the derivation would not be circular, only unsupported. Overall, the derivation chain is self-contained for the claims it makes, with benchmarks and prior results used as inputs rather than as conclusions.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

No parameters are fitted and no new physical entities are postulated. All constructions are explicit finite point sets or periodic point sets with coordinates in the paper. The uncharged inputs are standard lattice facts, the uniqueness of a cited binary code, and the reliability of the paper's own computer searches.

assumptions (3)

ad hoc to paper The depth-first search enumerations in Sections 3, 4.2, and 5 are complete and correctly implement the stated extension criteria.
Theorem 4.3, the claim that Q5 and R5 have no six-dimensional extension with 72 points, and the assertion that exactly eight alternate triples exist in Section 5 all rest on finite computer searches whose correctness is not formally proved. The code is provided, but the searches are treated as black boxes.
domain assumption The four-coloring constraints in Section 4.1 are exactly equivalent to non-overlap of the constructed five-dimensional spheres.
The packing density and validity of the construction depend on the distance rules between same, adjacent, and opposite colors; the paper states 'one can check' rather than deriving the equivalence in full.
domain assumption The uniqueness of the binary (9,4,4) constant-weight code cited from Ostergard [18].
Section 5 uses 'such a code is unique' to justify the description of the Leech-Sloane configuration; if this uniqueness were false, the layer analysis would need to consider multiple codes.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Variations on five-dimensional sphere packings." pith.science (2026). https://pith.science/paper/SGMUIAXZ

@misc{pith2026241200937,
  author       = {Pith},
  title        = {Pith review of: Variations on five-dimensional sphere packings},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SGMUIAXZ}},
  note         = {Machine review of arXiv:2412.00937}
}

read the original abstract

We analyze Sz\"oll\H{o}si's recent construction of a conjecturally optimal five-dimensional kissing configuration and produce a new such configuration, the fourth to be discovered. We construct five-dimensional sphere packings from these configurations, which augment Conway and Sloane's list of conjecturally optimal packings. We also construct a new kissing configuration in nine dimensions. None of these constructions improves on the known records, but they provide geometrically distinct constructions achieving these records.

Figures

Figures reproduced from arXiv: 2412.00937 by the authors.

**Figure 1.1.** The centers of the spheres in the face centered cubic kissing arrangement on the left, and the centers of the spheres in the hexagonal close packing kissing arrangement on the right. To produce the arrangement on the right from the one on the left, the top layer is deleted and the bottom layer is reflected across the central layer (the hexagon). their symmetry groups act transitively on the spheres. Only four such p… view at source ↗

**Figure 4.1.** The four possible ways to arrange triangles ∆1 and ∆2 around a point, labeled a through d. In arrangements a and b, two of the neighboring points are labeled p and q. 0 1 2 3 2 3 0 1 0 1 2 3 2 3 0 1 0 1 2 3 0 1 0 1 2 3 2 3 0 1 0 1 2 3 2 3 0 1 0 1 [PITH_FULL_IMAGE:figures/full_fig_p009_4_1.png] view at source ↗

**Figure 4.2.** The uniform packings with kissing configuration Q5 (on the left) and R5 (on the right). The local analysis from [PITH_FULL_IMAGE:figures/full_fig_p009_4_2.png] view at source ↗

Figures from the paper (1 more)

**Figure 4.3.** Figure 4.3: The irregular tetrahedron and octahedron with ∆1 facets, unfolded into nets. properties. For example, one octahedron and four tetrahedra can be assembled to form a larger tetrahedron (with doubled edge lengths, and with the tetrahedra nestled in the corners of the la…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Linear Programming Bounds for Fibered Sphere Packings
math.MG 2026-07 conditional novelty 8.0 of 10

Linear programming bounds are sharp for some fibered sphere packings, collapse to the planar bound in a key six-dimensional case, and fail to prove the Cohn–Rajagopal conjecture for D5/A3.

Reference graph

Works this paper leans on

23 extracted references · 18 canonical work pages · cited by 1 Pith paper

[1]

Alexei Andreanov and Yoav Kallus, Locally optimal 2-periodic sphere packings , Discrete Comput. Geom. 63 (2020), no. 1, 182–208. arXiv:1704.08156 doi:10.1007/s00454-019-00150-6

work page Pith review arXiv 2020
[2]

Eiichi Bannai and N. J. A. Sloane, Uniqueness of certain spherical codes , Canadian J. Math. 33 (1981), no. 2, 437–449. doi:10.4153/CJM-1981-038-7

work page doi:10.4153/cjm-1981-038-7 1981
[3]

Henry Cohn, Yang Jiao, Abhinav Kumar, and Salvatore Torquato, Rigidity of spherical codes , Geom. Topol. 15 (2011), no. 4, 2235–2273. arXiv:1102.5060 doi:10.2140/gt.2011.15.2235

work page Pith review arXiv 2011
[4]

The sphere packing problem in dimension 24

Henry Cohn, Abhinav Kumar, Stephen D. Miller, Danylo Radchenko, and Maryna Viazovska, The sphere packing problem in dimension 24 , Ann. of Math. (2) 185 (2017), no. 3, 1017–1033. arXiv:1603.06518 doi:10.4007/annals.2017.185.3.8

work page Pith review arXiv 2017
[5]

J. H. Conway and N. J. A. Sloane, What are all the best sphere packings in low dimensions? , Discrete Comput. Geom. 13 (1995), no. 3-4, 383–403. doi:10.1007/BF02574051

doi:10.1007/bf02574051 1995
[6]

Optimality and uniqueness of the $D_4$ root system

David de Laat, Nando M. Leijenhorst, and Willem H. H. de Muinck Keizer, Optimality and uniqueness of the D4 root system, preprint, 2024. arXiv:2404.18794 V ARIATIONS ON FIVE-DIMENSIONAL SPHERE PACKINGS 17

work page Pith review arXiv 2024
[7]

Pi 5 (2017), e2, 29

Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the...

arXiv 2017
[8]

Hales, A proof of the Kepler conjecture , Ann

Thomas C. Hales, A proof of the Kepler conjecture , Ann. of Math. (2) 162 (2005), no. 3, 1065–1185. doi:10.4007/annals.2005.162.1065

doi:10.4007/annals.2005.162.1065 2005

Show all 23 references

[9]

Korkine and G

A. Korkine and G. Zolotareff, Sur les formes quadratiques , Math. Ann. 6 (1873), no. 3, 366–389. doi:10.1007/BF01442795

doi
[10]

Greg Kuperberg, Notions of denseness , Geom. Topol. 4 (2000), 277–292. arXiv:math/9908003 doi:10.2140/gt.2000.4.277

2000 arXiv
[11]

John Leech, Five dimensional non-lattice sphere packings , Canad. Math. Bull. 10 (1967), 387–393. doi:10.4153/CMB-1967-037-5

1967 doi
[12]

, Six and seven dimensional non-lattice sphere packings , Canad. Math. Bull. 12 (1969), 151–155. doi:10.4153/CMB-1969-014-1

1969 doi
[13]

John Leech and N. J. A. Sloane, Sphere packings and error-correcting codes , Canadian J. Math. 23 (1971), 718–745. doi:10.4153/CJM-1971-081-3

1971 doi
[14]

V. I. Levenˇ ste ˘ ın,On bounds for packings in n-dimensional Euclidean space, Dokl. Akad. Nauk SSSR 245 (1979), no. 6, 1299–1303

1979
[15]

Mittelmann and Frank Vallentin, High-accuracy semidefinite programming bounds for kissing numbers , Experiment

Hans D. Mittelmann and Frank Vallentin, High-accuracy semidefinite programming bounds for kissing numbers , Experiment. Math. 19 (2010), no. 2, 175–179. arXiv:0902.1105 doi:10.1080/10586458.2010.10129070

2010 arXiv
[16]

Musin, The kissing number in four dimensions , Ann

Oleg R. Musin, The kissing number in four dimensions , Ann. of Math. (2) 168 (2008), no. 1, 1–32. arXiv:math/0309430 doi:10.4007/annals.2008.168.1

2008 arXiv
[17]

A. M. Odlyzko and N. J. A. Sloane, New bounds on the number of unit spheres that can touch a unit sphere in n dimensions, J. Combin. Theory Ser. A 26 (1979), no. 2, 210–214. doi:10.1016/0097-3165(79)90074-8

1979 doi
[18]

Patric R. J. ¨Osterg ˚ ard,Classification of binary constant weight codes , IEEE Trans. Inform. Theory 56 (2010), no. 8, 3779–3785. doi:10.1109/TIT.2010.2050922

2010
[19]

Sch¨ utte and B

K. Sch¨ utte and B. L. van der Waerden,Das Problem der dreizehn Kugeln , Math. Ann. 125 (1953), 325–334. doi:10.1007/BF01343127

1953 doi
[20]

Ferenc Sz¨ oll˝ osi,A note on five-dimensional kissing arrangements , Math. Res. Lett. 30 (2023), no. 5, 1609–1615. arXiv:2301.08272 doi:10.4310/MRL.2023.v30.n5.a13

2023 arXiv
[21]

Axel Thue, Om nogle geometrisk-taltheoretiske Theoremer, Forhandlingerne ved de Skandi- naviske Naturforskeres 14 (1892), 352–353
[22]

Viazovska, The sphere packing problem in dimension 8 , Ann

Maryna S. Viazovska, The sphere packing problem in dimension 8 , Ann. of Math. (2) 185 (2017), no. 3, 991–1015. arXiv:1603.04246 doi:10.4007/annals.2017.185.3.7

2017 arXiv
[23]

Chuanming Zong, Sphere packings, Universitext, Springer-Verlag, New York, 1999. doi:10.1007/b98975 Microsoft Research New England, One Memorial Drive, Cambridge, MA 02142, USA Email address : cohn@microsoft.com Department of Mathematics, Massachusetts Institute of Technology, ...

1999 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [1]

Alexei Andreanov and Yoav Kallus, Locally optimal 2-periodic sphere packings , Discrete Comput. Geom. 63 (2020), no. 1, 182–208. arXiv:1704.08156 doi:10.1007/s00454-019-00150-6

work page Pith review arXiv 2020

[2] [2]

Eiichi Bannai and N. J. A. Sloane, Uniqueness of certain spherical codes , Canadian J. Math. 33 (1981), no. 2, 437–449. doi:10.4153/CJM-1981-038-7

work page doi:10.4153/cjm-1981-038-7 1981

[3] [3]

Henry Cohn, Yang Jiao, Abhinav Kumar, and Salvatore Torquato, Rigidity of spherical codes , Geom. Topol. 15 (2011), no. 4, 2235–2273. arXiv:1102.5060 doi:10.2140/gt.2011.15.2235

work page Pith review arXiv 2011

[4] [4]

The sphere packing problem in dimension 24

Henry Cohn, Abhinav Kumar, Stephen D. Miller, Danylo Radchenko, and Maryna Viazovska, The sphere packing problem in dimension 24 , Ann. of Math. (2) 185 (2017), no. 3, 1017–1033. arXiv:1603.06518 doi:10.4007/annals.2017.185.3.8

work page Pith review arXiv 2017

[5] [5]

J. H. Conway and N. J. A. Sloane, What are all the best sphere packings in low dimensions? , Discrete Comput. Geom. 13 (1995), no. 3-4, 383–403. doi:10.1007/BF02574051

doi:10.1007/bf02574051 1995

[6] [6]

Optimality and uniqueness of the $D_4$ root system

David de Laat, Nando M. Leijenhorst, and Willem H. H. de Muinck Keizer, Optimality and uniqueness of the D4 root system, preprint, 2024. arXiv:2404.18794 V ARIATIONS ON FIVE-DIMENSIONAL SPHERE PACKINGS 17

work page Pith review arXiv 2024

[7] [7]

Pi 5 (2017), e2, 29

Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the...

arXiv 2017

[8] [8]

Hales, A proof of the Kepler conjecture , Ann

Thomas C. Hales, A proof of the Kepler conjecture , Ann. of Math. (2) 162 (2005), no. 3, 1065–1185. doi:10.4007/annals.2005.162.1065

doi:10.4007/annals.2005.162.1065 2005