| n | Enclosure of the continuous optimum | Nine-decimal optimum (exact) |
|---|---|---|
| 1 | [0.688190960235586769103604790955, 0.688190960235586769103604790956]√(25 + 10√5)/10 | 0.688190959 |
| 2 | [0.760845213036122857693151466703, 0.760845213036122857693151466704]√(10 + 2√5)/5 | 0.760845212 |
| 3 | [1.034563887852745238722502573982, 1.034563887852745238722502573983] | 1.034563887 |
| 4 | [1.250988879234854835726034468650, 1.250988879234854835726034468651] | 1.250988878 |
| 5 | [1.447980550405670367298603865867, 1.447980550405670367298603865868]5/(2√(5 − 2√5) + 2) | 1.447980549 |
| 6 | [1.651074770596782374034569505953, 1.651074770596782374034569505954](4 + 1/sin 36°)/(2√(5 − 2√5) + 2) | 1.651074767 |
| 7 | [1.740983299207393612609980566106, 1.740983299207393612609980566107] | 1.740983297 |
| 8 | [1.852488899111271345913487762578, 1.852488899111271345913487762579] | 1.852488896 |
Truncating the continuous optimum does not give the grid optimum. For n = 6 the truncation is 1.651074770, but the centres must also lie on the grid, giving a maximum of 1.651074767. For n = 3–8 the continuous maximiser is also unique up to pentagon symmetries and circle relabelling. No uniqueness claim is made for grid maximisers, and n ≥ 9 is outside this result.
Proof outline
Write a = cot(π/5)/2 and R = 1/(2sin(π/5)) for the inradius and circumradius. Feasible centres for radius r form the scaled pentagon (1−r/a)P. One circle satisfies r ≤ a. For two circles, separation and the triangle inequality give S ≤ R(2−S/a), hence S ≤ 2aR/(a+R), attained by the incircle and a corner circle.
The candidates for n = 3, 5, 6 have radical expressions. For n = 4, 7, 8, contact equations and rational isolating boxes define the candidates. Interval arithmetic verifies the Banach fixed-point conditions, positive radii, containment and inactive-contact clearances, establishing exact roots and feasible constructions.
The global argument chooses a longest centre pair, moves its direction into [π/10,3π/10] by pentagon symmetry, and enumerates how many remaining centres lie on either side. The n = 3–6 models order same-side circles by radius; n = 7–8 instead use polar angle. Complete direction partitions retain a root-to-leaf path for every real packing. Walls, directions, separation and previously proved subset bounds give necessary linear constraints.
For Az ≤ b and a known variable box B, any nonnegative rational y gives c·z ≤ y·b + max(z∈B)(c−Aᵀy)·z. The verifier recomputes this bound with outward-rounded rational intervals, including every coefficient residual. A solver’s infeasibility status is not proof. Every split must be complete; ordinary leaves require a strict bound or contradiction certificate.
The remaining leaves localise every competitive packing near a candidate root. Normalising a nonzero perturbation by its largest component produces a component of absolute value one. A local model with rigorous Taylor remainders bounds every component strictly below one, excluding any distinct same-or-better configuration. This completes the continuous global proof.
The grid proof returns to the site’s unrotated coordinate frame and checks integer neighbourhoods in all ten symmetry orientations; the n = 5 circle set is itself invariant, so one neighbourhood suffices. Integer partitions and strict contradiction certificates exclude every score at least one grid step higher. All eight witnesses pass the site’s existing exact verifier and attain the tabulated grid bounds.
Reproduction materials
- Complete proof package (ZIP, approximately 309 MB)
- Author’s guide (PDF, Chinese)
- Eight nine-decimal witnesses (JSON)
- Site replay results (JSON)
SHA-256: d7f8c7b77179193dd6bcd8d76619c2d88765257791f4538e4559bf722bc99ddd
python verify_proofs.py --output replay_result.jsonUse Python 3.10 or newer, without -O or -OO. Only the standard library is required; allow at least 4 GB of temporary disk space. --quick checks integrity and witnesses, not the full proof. Systems supporting fork and pread can add --workers 3.
The site reviewed the geometric reduction, interval arithmetic, local rigidity and lattice-exclusion code, then ran the submitted verifiers from scratch without reusing prior audit conclusions. Single-process Windows replay took about 28 minutes; all 1,044,679 global nodes and 353,596 lattice nodes for n = 8 passed. The existing site verifier separately checked every witness. This is a computer-assisted proof review, not proof-assistant kernel verification.
Credit and adoption
zzzcy #308 submitted the proof; the site reviewed it and prepared this bilingual account, awarding one +2 proof contribution. Existing constructions retain their attribution to Jonathan Viquerat and other discoverers in Friedman’s table. Ninjbat (2016) already gives a general theorem covering the continuous two-circle case. No first-discovery or historical first-proof claim is made here.
Erich Friedman: Circles in Pentagons · Ninjbat (2016)
Competition closes for n = 1–8 under the existing proven-optimum mechanism. Historical submissions and record holders remain; attached witnesses do not automatically replace player records.