The Reinhardt conjecture in Lean 4

The Reinhardt conjecture in Lean 4

A Lean 4 proof that Reinhardt's smoothed octagon packs the plane worst among centrally symmetric convex shapes, and that it is the only worst shape, up to affine maps.

GitHub repository vltanh/lean4-smoothed-octagon GitHub repository vltanh/lean4-smoothed-octagon

Copies of a disk, packed as tightly as possible, cover \(\pi/\sqrt{12} = 90.69\ldots\%\) of the plane, while squares and regular hexagons cover all of it. In 1934 Karl Reinhardt conjectured that among centrally symmetric convex shapes, those that look the same after a half turn, the one that packs worst is the smoothed octagon, a regular octagon whose corners are cut off by arcs of hyperbolas. Its densest packing has density

\[\delta_{\mathrm{oct}} = \frac{8 - 4\sqrt2 - \log 2}{2\sqrt2 - 1} = 0.902414\ldots,\]

and he conjectured that it is the only worst shape, up to affine maps. Kurt Mahler reached the same octagon independently in 1947. This project proves both in Lean 4: every centrally symmetric convex shape has a packing of density at least \(\delta_{\mathrm{oct}}\), and equality holds only for the images of the smoothed octagon under invertible affine maps.

Copies of the smoothed octagon in a densest packing, sliding past each other while each keeps touching its neighbours
The smoothed octagon in its densest packing. The copies slide through a continuum of densest packings, and each keeps touching its six neighbours.

pack shapes yourself and try to beat the octagon →

The smoothed octagon

Take the regular octagon whose sides lie on the lines \(x \cos(k\pi/4) + y \sin(k\pi/4) = 1\), \(k = 0, \dots, 7\). At each corner, extend the two sides next to the corner’s sides, and replace the corner by an arc of the curve along which the product of the distances \(d\) and \(d'\) to these two lines is \(\sqrt2/4\). The curve is a hyperbola with the two lines as asymptotes. At the corner of the sides \(x = 1\) and \(x + y = \sqrt2\), it is

\[(1 - y)(\sqrt2 - x + y) = \tfrac12,\]

and it touches the two sides at \((1, 1 - 1/\sqrt2)\) and \((\sqrt2 - \tfrac12, \tfrac12)\). The constant \(\sqrt2/4\) is the one for which the curve touches both sides without crossing them, so the boundary has no corners left. Each side keeps a straight middle part of length \(2 - \sqrt2\).

A regular octagon with one corner rounded by the hyperbola that touches the two sides at the corner and approaches the lines of the next two sides, with the corner magnified
One corner of the regular octagon, cut off by the hyperbola that touches its two sides and approaches the next two (dashed). The product of the distances to the two dashed lines is constant along the curve.

For a centrally symmetric convex shape, László Fejes Tóth proved in 1950 that no packing beats the best lattice packing, where the copies sit at the points of a grid of parallelograms. The best lattice packing comes from the hexagon of least area among the affine images of a regular hexagon inscribed in the shape, and the copies touch at its corners. The regular octagon already packs worse than the disk, which Mahler called “rather surprising”, and rounding its corners makes it worse still. Unlike the disk’s, the smoothed octagon’s densest packings come in a continuum: every such hexagon inscribed in it has the same area.

Densest packings of the disk, the regular octagon, the smoothed 14-gon and the smoothed octagon, with densities 0.906900, 0.906164, 0.906052 and 0.902414
The disk, the regular octagon, the smoothed 14-gon and the smoothed octagon, all of inradius 1, each in front of its densest packing.

The smoothed 14-gon in the figure belongs to the same family as the octagon. Hales showed in 2017 that the smoothed regular polygons with \(6k + 2\) sides, \(8, 14, 20, \dots\), are all Pontryagin extremals of his control problem: they satisfy the conditions that Pontryagin’s maximum principle sets for a worst shape. Their densities increase with \(k\) towards the disk’s \(\pi/\sqrt{12}\), and the octagon’s is the least: \(0.902414\) for \(k = 1\), \(0.906052\) for \(k = 2\), just below the regular octagon’s \(0.906164\), and \(0.906607\) for \(k = 3\). Hales and Vajjha found no other extremals, and they wrote in 2024 that “a proof that no other extremals exist would complete a proof of the Reinhardt conjecture”.

The statements

The project proves three theorems. They are stated in a Challenge file that imports only Mathlib, with two kinds of definitions copied word for word: the packing definitions of lean4-smoothed-polygon, a formalization of Hales and Vajjha’s book Packings of Smoothed Polygons on which this project builds, and Reinhardt’s construction of the smoothed octagon above. The density of a shape is the supremum of the densities of packings of the plane by congruent copies of it. The three theorems say:

  • the smoothed octagon is a centrally symmetric convex disk whose greatest packing density is \(\delta_{\mathrm{oct}}\);
  • every centrally symmetric convex disk has greatest packing density at least \(\delta_{\mathrm{oct}}\);
  • equality holds exactly for the images of the smoothed octagon under invertible affine maps.

The library also proves the control form of the conjecture: every trajectory of Hales’s control problem with the boundary conditions costs at least \(\sqrt{12}\,\delta_{\mathrm{oct}}\).

The proof, in brief

Following Thomas Hales, the problem becomes a problem of optimal control on \(\mathrm{SL}_2(\mathbb{R})\). A worst shape, normalized so that the hexagon of its densest packing is regular, is traced by six points that slide along its boundary, and its area is the cost of the trajectory they follow. Conversely, every trajectory of cost below \(\pi\) bounds such a shape.

The six contact points of the smoothed octagon moving around its boundary, with the six neighbouring copies of its densest packing
The six points where the smoothed octagon touches its neighbours move around its boundary through one period of its trajectory, and the six neighbouring copies move with them.

The proof has five stages. The foundations show that the conjecture is equivalent to a lower bound on the cost of every admissible trajectory, and that a worst shape gives a global minimizer of the control problem. The reduction shows that a global minimizer stays in a compact part of the state space, lifts to a Pontryagin extremal (proved in lean4-smoothed-polygon from the maximum principle of lean4-optimal-control), switches between the three vertices of the control simplex finitely many times, and is normal. Read around a period, the switches then fall into five classes when there are six or more pieces, and each class is excluded. A period with at most five pieces costs at least \(\sqrt{12}\,\delta_{\mathrm{oct}}\), with equality only for the octagon’s four-piece control with equal durations. Finally, a worst shape has the octagon’s trajectory, so it is a linear image of the octagon, and conversely linear images of the octagon pack equally badly.

Verification

Lean’s kernel checks every proof. Nothing is assumed beyond Lean’s three standard axioms, propext, Classical.choice and Quot.sound. The three theorems are stated in a Challenge file, and the root of the library restates them word for word and proves them, with no hypothesis and no sorry. An audit checks that all 8,295 declarations of the library depend only on the standard axioms, and Comparator, the checker of the Palomar registry, confirms that the proof establishes exactly the Challenge’s statements, under Lean’s kernel and the independent NanoDa kernel.

The scalar estimates of the proof are inequalities, polynomial identities, monotonicity and convexity arguments; a few polynomial signs are checked by explicit Bernstein expansions. A full build takes about 18 minutes on 20 cores.

Prior work

Reinhardt posed the problem in 1934 and proposed the smoothed octagon. Mahler, independently, proved in 1946 that every centrally symmetric convex shape packs at least \(\sqrt3/2\), and in 1947 that a worst shape exists and that among octagons the regular one is worst; he built the smoothed octagon as “possibly even” the answer. Walter Ledermann and Mahler named it in 1949. Fejes Tóth reduced the problem to lattice packings in 1950. V. Ennola and P. P. Tammela raised the lower bound to \(0.88\) in 1961 and to \(0.892656\) in 1970, and F. L. Nazarov proved in 1986 that the smoothed octagon is a local minimum. Hales recast the problem in the calculus of variations in 2011 and as optimal control in 2017, and in 2024 Hales and Koundinya Vajjha proved in Packings of Smoothed Polygons that a worst shape is a smoothed polygon with finitely many sides, Mahler’s first conjecture, adding that Reinhardt’s conjecture “remains open”. lean4-smoothed-polygon formalizes the parts of their book that this proof uses, and the repository’s prior-work notes give the full history with references.

Contributors

The proof was written in the repository. ChatGPT Pro drafted the argument, starting from Hales’s formulation of the problem as optimal control and from Hales and Vajjha’s book. Claude Opus 5.5, in Claude Code, wrote the Lean proof and organized it, with sub-agents that stated and proved the stages in parallel, and wrote the figures, the playground and the documentation, following my skill for formalizing papers, formalize-math-paper. I chose the problem and directed the work. The proof builds on two of my Lean libraries, lean4-smoothed-polygon and lean4-optimal-control, the second for Filippov’s theorem and the Pontryagin maximum principle.

References