Motivation

Packing congruent circles into a square is a classical problem in discrete geometry: for each natural number $n$, choose a common radius as large as possible while keeping all disks inside the square and preventing overlap. Every exact value requires two logically distinct achievements: an explicit configuration attaining the proposed radius and a proof that no configuration can do better.

The character of those proofs changes sharply with $n$. The first cases admit short geometric arguments; later cases use contact-graph analysis, specialized case divisions, or computer-assisted global optimization with interval arithmetic. Formalizing the resulting constants therefore provides a growing benchmark for extremal geometry, real algebra, finite configurations, and verified computation in Lean.

This is an open-ended formalization mission. It begins with the exact constants currently represented by theorem-backed milestones, but it is not restricted to a fixed terminal value of $n$. Further milestones may be added whenever an exact packing value and its rigorous optimality argument are identified and stated precisely enough for formalization.

Setting

A point is a pair of real coordinates. For points $p=(x,y)$ and $q=(x',y')$, squared Euclidean distance is

$$\operatorname{sqDist}(p,q)=(x-x')^2+(y-y')^2.$$

For a real radius $r$, a point lies in the inner square when both coordinates belong to the closed interval $[r,1-r]$. This is exactly the coordinate condition saying that a closed disk of radius $r$, centered at that point, is contained in the unit square.

The predicate $\operatorname{Packable}(n,r)$ requires $0\le r\le \tfrac12$ and a family of $n$ centers in the inner square such that the squared distance between every two distinctly indexed centers is at least $(2r)^2$. Equality is allowed, so tangent disks are admitted. Radius zero is also admitted.

Define

$$r_n=\sup\{r\in\mathbb R:\operatorname{Packable}(n,r)\}$$

and define the optimal covered-area fraction by

$$c_n=n\pi r_n^2.$$

It is often convenient to use the equivalent point-separation constant $d_n$, the greatest possible minimum pairwise distance among $n$ points in the unit square. The conversion is

$$r_n=\frac{d_n}{2(1+d_n)}, \qquad c_n=n\pi\left(\frac{d_n}{2(1+d_n)}\right)^2.$$

The Lean definitions use a supremum rather than assuming in advance that an optimal packing is attained.

Current exact-value milestones

The mission currently contains theorem-backed milestones for the following values:

$n$	Exact separation or area value	Proof character in the supplied notes
$2$	$d_2=\sqrt2$, hence $c_2=\pi(3-2\sqrt2)$	diagonal bound
$3$	$d_3=\sqrt6-\sqrt2$	minimum enclosing square of a triangle
$4$	$d_4=1$, hence $c_4=\pi/4$	convex hull and perimeter
$5$	$d_5=1/\sqrt2$	four-cell pigeonhole argument
$6$	$d_6=\sqrt{13}/6$	case-specific geometric proof
$7$	$d_7=4-2\sqrt3$	hand proof and later computer verification
$8$	$d_8=\sqrt{2-\sqrt3}$	case-specific geometric proof
$9$	$d_9=1/2$, hence $c_9=\pi/4$	classical geometric proof
$16$	$d_{16}=1/3$, hence $c_{16}=\pi/4$	theoretical grid-optimality proof
$25$	$d_{25}=1/4$, hence $c_{25}=\pi/4$	theoretical grid-optimality proof
$36$	$d_{36}=1/5$, hence $c_{36}=\pi/4$	theoretical grid-optimality proof

For rows stated using $d_n$, the corresponding milestone for $c_n$ uses the conversion formula above. The equalities are claims about the supremum-defined packing constants, not merely about the displayed candidate configurations.

An extensible mission

The milestone list is intended to grow. The supplied survey notes classify $n=2,\ldots,33$ and $n=36$ as rigorously solved in the cited literature, while distinguishing $n=34$ and $n=35$ as not rigorously closed in the cited 2021 account. Many of the computer-assisted cases do not have a simple radical expression in the supplied notes. Before such a case is linked to a Lean theorem, its primary source must provide a precise candidate value, algebraic characterization, certified enclosure, or optimal-configuration certificate that can be stated faithfully.

A new milestone should identify:

1. the precise value or exact characterization being formalized;
2. an attaining configuration or a certified existence argument;
3. a universal upper bound or global-optimality certificate;
4. the primary source and exact theorem, equation, or certificate location;
5. any trusted computational artifact and the arithmetic guarantees it requires.

Numerical evidence and strong bounds are valuable, but they must be labeled as bounds rather than exact-value milestones. Conversely, newly published exact results for larger $n$ may be added without changing the underlying definitions.

Proof obligations

Every exact-value milestone must connect the proposed value to Packable, r_n, and c_n. Constructing a configuration establishes only a lower bound. An upper-bound argument without attainability also does not establish equality. A complete proof must bridge both directions through the supremum definition.

The proof methods may include:

• elementary diameter, pigeonhole, convexity, or enclosing-shape arguments;
• normalization between disk centers and point-separation configurations;
• contact-graph and boundary-constraint analysis;
• finite case decompositions;
• interval arithmetic and formally checked branch-and-bound certificates;
• exact algebraic identities needed to convert $d_n$ into $r_n$ and $c_n$.

Shortcuts that redefine $r_n$, $d_n$, or $c_n$ to equal a desired answer are excluded. The constants must remain consequences of the common geometric model.

Mission structure

The root theorem CirclePackingConstants.c_all is the conjunction of the eleven exact-value milestones currently in the mission, covering $n=2,3,4,5,6,7,8,9,16,25,36$. Its proof sketch reduces the root directly to those milestone theorems, so the mission remains open until every current exact value is proved.

The milestone theorems remain separately reusable and independently auditable. When further exact values are added, a successor aggregate theorem can extend the conjunction and become the new root without replacing the shared definitions or invalidating earlier results.

This structure allows elementary cases, historical hand proofs, and computer-assisted certificates to progress independently while remaining part of one cumulative library of exact circle-packing constants.

Formalization scope

The Lean model uses ℝ × ℝ for points and an explicit coordinate formula for squared Euclidean distance. Disk containment is represented by inclusive coordinate inequalities. Nonoverlap is represented by a weak squared-distance inequality, so tangency is permitted. The indexing type is Fin n, and the definitions apply to every natural number, including zero.

The definition bundle contains only Point, sqDist, InInnerSquare, Packable, r_n, and c_n. Solvers may introduce normalization maps, separation bounds, explicit configurations, supremum lemmas, contact structures, certificate checkers, and radical or polynomial identities as auxiliary declarations.

Selected references

• User-supplied notes, Circles in squares: constants, proofs, and what is actually known, supplied September 12, 2026. The notes summarize the exact small-$n$ formulas, grid cases, historical proof taxonomy, and computer-assisted frontier used to organize this mission.
• J. Schaer and A. Meir, “On a geometric extremum problem,” Canadian Mathematical Bulletin 8 (1965), 21–27.
• J. Schaer, “The densest packing of nine circles in a square,” Canadian Mathematical Bulletin 8 (1965), 273–277.
• B. L. Schwartz, “Separating points in a square,” Journal of Recreational Mathematics 3 (1970), 195–204.
• J. B. M. Melissen, “Densest packing of six equal circles in a square,” Elemente der Mathematik 49 (1994), 27–31.
• M. C. Markot, “Improved interval methods for solving circle packing problems in the unit square,” Journal of Global Optimization 81 (2021), 773–803.
• Erich Friedman, Circles in Squares, Erich's Packing Center, for background tables and diagrams of candidate packings.