Playground
Squares and hexagons can tile a floor with nothing left over. Disks can't: packed as tightly as possible, they cover 90.69% of the plane. In 1934 Karl Reinhardt asked which shape packs worst, among the convex shapes that look the same after a half turn, and he guessed this one: a regular octagon with its corners rounded off by hyperbolas. Its densest packing covers 90.24%. The conjecture was open for ninety years, and it is now proved in Lean 4: no shape of this kind packs worse.
1
Pick a shape and drag the orange and the green copy. The other copies follow, so they always sit on a lattice, a grid of equal parallelograms. Copies can't overlap, so squeezing them together finds the densest packing. For shapes like these, László Fejes Tóth proved in 1950 that the best lattice packing is as good as any packing.
Drag the orange or the green copy; it stops where it meets another copy and slides along it.
2
Reinhardt’s shape starts as a regular octagon, and each corner is cut off along a curve. Step through one corner, then all eight.
In steps 3 and 4, drag the point along the curve.
Hales showed in 2017 that the smoothed octagon belongs to a family. The smoothed regular polygons with 6k + 2 sides (8, 14, 20, …) are all Pontryagin extremals of his control problem: they satisfy the conditions that Pontryagin's maximum principle sets for a worst shape. Their densities grow with k towards the disk's, and the octagon's is the least. No other extremals have been found, and Hales and Vajjha wrote in 2024 that a proof that none exist would complete a proof of the conjecture.
3
No convex shape that looks the same after a half turn packs worse than the smoothed octagon: Reinhardt conjectured it, and the Lean proof shows it. See how close you can get: drag the corners of the dark shape and watch its densest packing rearrange around it.
Drag a corner; the opposite corner moves with it, and the shape stays convex. Click an edge to add a pair of corners there.
With eight corners you can't win: Mahler proved in 1947 that no octagon of this kind packs worse than the regular one. In 1949 Ledermann and Mahler found the worst decagon, at 90.54%, and it is not the regular one. Polygons with more corners get closer to 90.24%, and none gets below it: that is Reinhardt's conjecture, now proved in Lean 4. Near the smoothed octagon itself, Nazarov had proved in 1986 that every shape close enough to it packs at least as densely.
Inscribe in the shape a hexagon with corners p, q, q − p, −p, −q, p − q, all on its boundary. Copies of the shape centred at the points 2(ip + jq), for all whole numbers i and j, then form a packing in which every copy touches six others, at the corners of the hexagon. The densest lattice packing comes from the hexagon of least area (Minkowski, Reinhardt, Mahler), and its density is three times the area of the shape over four times the area of the hexagon. The page tries every starting corner p on the boundary, finds q by bisection, and keeps the smallest hexagon.
4
Every shape of this kind has packings in which each copy touches six others, and they can slide: move one corner of the inscribed hexagon along the boundary and the whole packing shifts. For most shapes the density changes as it slides. For the smoothed octagon it stays the same, so all these packings are densest.
Drag the slider or press Play. The dots are where the middle copy touches its six neighbours.
5
From 1934 to now. Pick a date to see how far the proved lower bound had come.