Experiment · Geometry

Packomania: exact, certified circle packings

This experiment addresses a classic geometry problem: place N circles of free radii in a square, without overlap, so that the sum of the radii is as large as possible. The referee is the Packomania “csqv” table. Outcome: 367 of the 583 entries of the table come from the experiment. Each packing is exact, comes with a certificate that anyone can recheck, and rechecks identically. A proven bound serves as a ruler: the entries from the experiment reach 92.7 % to 94.3 % of that bound.

1. The question

For each number N of circles, what is the largest sum of radii that fits in a unit square? Radii are free: each circle chooses its own size. No formula gives the answer; the table lists 583 entries (N from 1 to 500 except N = 493, and 84 larger values up to N = 10,000), each with the best known value and the packing that achieves it. The question of the experiment: establish exact, verifiable packings for a large number of entries.

2. Verification protocol

Each result is a file of N lines (x, y, r), submitted to the referee, who publishes it in his table, and checked by an exact checker independent of the program that produced the solution (section 5). The figures on this page are those of the table as read on the date given.

The referee and his site

Packomania is the site where Eckard Specht keeps the tables of the best known packings; the “csqv” table covers circles of free radii in a square. It rests on his program csqv (“2011–2026”, references page of the table) and on contributions from researchers: each entry carries the reference of its author, and the news of the page record each update with its date. On 4 Oct 2026 he notes there: “graphs with normed mean radius R(N) = sum_of_radii / N^1/2 versus N can be plotted, which show a nearly constant function. But there are slight periodic oszillations” (sic; packomania.com/csqv/csqv.html, news of 4 Oct 2026).

3. Results of the table

The three charts below are drawn from the values of the table of 30 Sep 2026 for N ≤ 500 (499 entries). Cyan dots mark the entries from the experiment, white rings the packings shown further down, the gold ring N = 69.

Three packings, drawn from the exact coordinates of the submitted entry: the centre and radius of every circle. Colour follows the radius, from violet (small) to cyan (large). Circles appear from left to right: this is a display sweep, unrelated to the computation. The data behind each figure can be downloaded as JSON.

4. A bound and the ratio of each entry

The table ranks entries against each other. A proven upper bound gives a fixed ruler: no packing of N disjoint circles in the unit square can exceed √(N/π) for the sum of radii. The ratio of each entry to this bound is read at the date of the table.

Theorem T1. For every packing of n pairwise disjoint circles contained in the unit square, Σ r_i ≤ √(n/π).

Proof. The discs are disjoint and contained in the square of area 1, so Σ π r_i² ≤ 1. By Cauchy–Schwarz applied to (r₁, …, r_n) and (1, …, 1), (Σ r_i)² ≤ n · Σ r_i² ≤ n/π. ∎

This bound is elementary: it takes two lines (area and Cauchy–Schwarz). Its proof is written above; it is not formalised in Lean. Here it serves as a yardstick for the whole table.

The bound check (distinct from the validity certificate of a packing) verifies π·(Σ r)² ≤ n in exact rational arithmetic only (no floating-point number enters the decision): π is bracketed by two rationals with 30 decimals, and the upper bound of π is the one used in the test. The ratio to the bound is returned as a rational bracket; no root is extracted to decide. On 11 Oct 2026, applied to the 583 entries of the table of 30 Sep 2026, it declares all of them compliant (published sum, 12 decimals). The entries from the experiment reach 92.7 % (N = 54) to 94.3 % (N = 426) of the bound; the whole table ranges from 73.4 % (N = 2) to 94.9 % (N = 10000). On the submitted files, in exact rationals: N = 54, 92.7 %; N = 69, 93.0 %; N = 101, 93.3 %; N = 200, 93.9 %; N = 500, 94.3 %.

This ratio does not change when a value in the table is beaten.

The refutation gate

A check is worth something only if it rejects what is false. The bound check has been tested on a 300-circle packing submitted on 24 Sep 2026: the bound √(300/π) is 9.7720502380583984; it accepts the real sum (9.188348093925) and rejects a sum fabricated just above the bound (9.7720502380584). It discriminates; it does not simply accept everything.

5. The validity certificate

The validity certificate is the exact check of the N lines of a file, run by a checker independent of the program that produced the solution. It uses neither square roots nor tolerance: the decimal values are read as rational numbers, and every comparison is made on those rationals.

Statement of validity

Proposition. Let (x_i, y_i, r_i), i = 1…N, be rational numbers, and let Q = [−½, ½]² be the square. If

1. for every i: r_i > 0, x_i − r_i ≥ −½, x_i + r_i ≤ ½, y_i − r_i ≥ −½ and y_i + r_i ≤ ½;
2. for every i < j: (x_i − x_j)² + (y_i − y_j)² ≥ (r_i + r_j)²;

then (a) each closed disc D_i with centre (x_i, y_i) and radius r_i lies inside Q; (b) the interiors of two distinct discs are disjoint (two discs meet in at most one point); (c) the sum of the radii of the N discs is exactly Σ r_i, a rational number computed without rounding.

Proof

(a) If (X, Y) belongs to D_i, then |X − x_i| ≤ r_i, so X ∈ [x_i − r_i, x_i + r_i] ⊂ [−½, ½] by condition 1; likewise for Y.

(b) If a point P lay in the interior of both D_i and D_j, the triangle inequality would give |c_i − c_j| ≤ |c_i − P| + |P − c_j| < r_i + r_j, hence |c_i − c_j|² < (r_i + r_j)², contradicting condition 2.

(c) It is a finite sum of rationals.

What the certificate guarantees

• that the N circles fit inside the square, with no excess, however small;
• that no pair of circles overlaps: at most, two circles touch;
• the exact value of the sum of radii of the submitted file;
• that exactly N circles are present.

The Lean theorems on file

For 62 submitted certificates, N = 54 among them, the conditions of the proposition above are written as theorems in the Lean proof assistant, instantiated on that packing (files CertN*.lean, no external library). Coordinates there are exact integers, at scale 10¹⁸. Replay of 11 Oct 2026 with Lean 4.30.0-rc2: each of the 310 theorems is evaluated by the kernel (decide +kernel) and Lean reports it as not depending on any axiom (“does not depend on any axioms”). These theorems concern particular packings (number of circles, inclusion, disjointness, sum, comparison with the earlier value), not the bound T1. Excerpt for N = 54:

-- Excerpt from CertN54.lean (N = 54, scale S = 10^18, circle = (x, y, r) in integers, square [0, S]²)
abbrev Inside (c : Int × Int × Int) : Prop :=
  0 < c.2.2 ∧ c.2.2 ≤ c.1 ∧ c.1 + c.2.2 ≤ S ∧ c.2.2 ≤ c.2.1 ∧ c.2.1 + c.2.2 ≤ S
abbrev Disj (c d : Int × Int × Int) : Prop :=
  (c.2.2 + d.2.2) * (c.2.2 + d.2.2) ≤
    (c.1 - d.1) * (c.1 - d.1) + (c.2.1 - d.2.1) * (c.2.1 - d.2.1)

theorem length_eq        : circles.length = 54                      := by decide +kernel
theorem all_inside       : ∀ c ∈ circles, Inside c                  := by decide +kernel
theorem pairwise_disjoint: circles.Pairwise Disj                    := by decide +kernel
theorem sum_eq           : sumR = 3842678286690508252               := by decide +kernel

The fifth theorem of the same file compares the sum with the value published before the submission (3.842635794975), see section 8.

Recheck it yourself

Download the JSON file of one of the packings, then run this short Python program (standard library only). It reads the coordinates as exact rationals, tests conditions 1 and 2 for every pair (N(N − 1)/2 pairs, that is 124,750 for N = 500) and prints the outcome.

import json
from fractions import Fraction as F

d = json.load(open("packomania_500.json"))
P = [tuple(F(v) for v in c) for c in d["circles"]]   # (x, y, r) en rationnels exacts
h = F(1, 2)
dedans = all(r > 0 and x - r >= -h and x + r <= h and y - r >= -h and y + r <= h for x, y, r in P)
disjoints = all((a[0]-b[0])**2 + (a[1]-b[1])**2 >= (a[2]+b[2])**2
                for i, a in enumerate(P) for b in P[i+1:])
print(len(P), dedans and disjoints, float(sum(r for _, _, r in P)))

Expected output for N = 500: 500 True 11.90174407201714. The JSON files also hold the sha256 fingerprint of the file submitted to the referee.

6. N = 69: a midline symmetry axis

Symmetric packings in the table usually have a diagonal of the square as their axis. On 20 September 2026 the referee notes for N = 69 an axis that is the midline between two opposite sides: “The candidate for N=69 is the very first which doesn't has a diagonal as a symmetry axes, but the midline between two opposite sides of the square. Are there more?” (sic). N = 70, with the same kind of axis, was found afterwards by Wilfred Heap, reference [17].

The animated figure shows entry N = 69, drawn from its coordinates: the 69 circles appear, then the vertical axis is drawn. To within 10⁻¹⁴ (largest measured deviation: 1.2 × 10⁻¹⁴), each circle left of the axis has its image on the right, with the same radius and at the same height. The diagram below compares a diagonal axis (here N = 34) with the midline case of N = 69.

7. The map of the challenge

The entries for N = 1 to 500, in rows of 20: the N of a cell is the starting number of its row plus its column minus 1 (the dotted cell, N = 493, has no entry). Horizontal rules separate the ranges of 100, with the count of entries from the experiment. At the bottom, the 84 entries with N > 500 (up to N = 10,000), in order. Table of 30 Sep 2026.

8. A packing improvement

On 16 Sep 2026, the table displayed for N = 54 a sum of radii of 3.842635794975 (value published in the table, coordinates rounded to 12 decimals, not rechecked in exact arithmetic, author not identified). The submitted entry, checked in exact arithmetic, has sum 3.842678286691, a gain of 4.25 × 10⁻⁵. The animation moves from the packing displayed by the table (violet) to that of the experiment (cyan): it is a display transition between two published states.

The submitted result is fixed: its sha256 is published, and anyone can recheck it identically.

9. What this question models

This type of question models placement problems that arise in cutting and packaging, placing antennas or sensors, studying granular materials and chip design. The csqv table is a common reference for comparing packings of circles of free radii. The packings shown here are exact, certified and rechecked by anyone.

My AI project in the service of my research

This challenge is not an end in itself: it is a test bench for my research on a certifiable embedded AI. My AI project, whose inner workings remain confidential, lets me reach 367 of the 583 entries in Packomania's "csqv" table, each packing rechecked in exact arithmetic. The certificate and the referee vouch for it: it is not my explanation you need to believe, it is the result, which can be checked again. This is the best known result at the date given, not a proven optimum.