Geometry · October 2026
Packing six
equilateral triangles
Six equilateral triangles of side 1 fit inside an equilateral container of side length
2.977081728299… for pieces of side 1
Maurizio Morandi found this packing in 2008. This preprint presents a computer-assisted proof that no arrangement fits in a smaller container, even when the pieces can move and rotate freely.
Preprint PDFPreprint · Not peer reviewed · Full theorem not formalized in Lean
Display coordinates are rounded. Exact arithmetic is used in the construction check below.
The question
What the proof adds to the known packing
The six pieces may move and rotate freely inside the container. A valid arrangement gives an upper bound on the required container size. A proof of optimality must also exclude every arrangement in a smaller container.
- Morandi’s construction · 2008
- s(6) ≤ TSix pieces fit at this size.
- This preprint’s claim
- s(6) ≥ TNo arrangement fits below this size.
Here, s(6) means the minimum container side. The two matching bounds give s(6) = T. The contribution is the lower-bound argument; the arrangement and its side length were already known.
Friedman’s catalogue credits the construction to Morandi. Chou’s 2016 manuscript recorded its optimality as unproved. Our literature search found no later published proof, but may have missed unpublished or unindexed work.
Proof method
How the proof covers all possible packings
Reduction to three fixed corner pieces
A geometric replacement argument shows that any hypothetical smaller packing can be converted into one with three aligned corner pieces. The other three triangles then lie in a central hexagon.
Coverage of the remaining positions and orientations
Each of the three remaining triangles has two position coordinates and one orientation, giving nine continuous variables. The certificate splits orientation intervals and encloses positions in polygons. Each branch includes its boundary, so the cases cover all configurations.
Exact geometric tests and rational linear certificates exclude impossible cases. The verifier checks each accepted calculation without repeating the numerical search that found it.
Local rigidity of the three inner pieces
The remaining cases lie near the reference construction. For a feasible packing at side T, a local theorem identifies the three inner pieces as a rotated or reflected copy of the reference triple. Together they touch all three container walls, which excludes a smaller container.
Corner piece B can move a short distance while the other pieces stay fixed. This motion does not allow a smaller container.
Certificate results
The verifier resolves all 11,165 terminal cases.
Select a case type to see how it is resolved. Bar widths show counts of terminal cases, not geometric volume or probability.
- Nodes in the closed cover
- 22,329
- Exact Farkas leaves
- 7,511
- Unresolved cases
- 0
Reproducibility
Checking the construction and the full proof
Construction check in the browser
The browser checker uses integer arithmetic in ℚ(√13). It checks 18 unit edges, 54 containment inequalities and separation of all 15 pairs of triangles, allowing contact.
It also verifies the rattler’s translation path. This certifies the construction, not the global lower bound.
Full certificate verification
Download or clone the repository, then run the verifier from its root. It uses Python 3.10 or newer and the standard library. No numerical solver is needed.
python3 tools/verify.pyThe full replay takes roughly 100 seconds on the reference system; other machines will vary. The repository includes the certificate, proof source, verification instructions and a separately implemented review route.
Repository and verification instructionsSupporting material
Preprint and supporting files
The preprint presents the geometric reductions, the local theorem and the finite certificate that connects them. Separately written verification programs provide an additional check of the computation.
The complete theorem has not been peer reviewed or formalized in Lean. A small Lean pilot checks one conditional linear branch of the certificate. The geometric arguments and the remaining programs still need to be correct. A successful browser check verifies the construction; it does not establish the lower bound.
Readers who want to examine the argument can use the review guide. It identifies the main proof steps, the checks already run, and the claims those checks do not establish.
Development and credits
The construction is credited to Maurizio Morandi in Friedman’s catalogue. The exploratory presentation is inspired by Yohei Nakajima’s soft-to-rigid packing project.
Kevin M. Neal developed this work with GPT-6 Astra, using Codex as the coding-agent harness and Pro mode in ChatGPT. These tools helped develop the arguments, write the code and manuscript, and review the calculations. The proof is computer-assisted because its argument depends on exact finite computations. The author is responsible for the claims and evidence. The AI reviews are not external peer review.