Prove2Me

Exact two-disk packing constant

Proved
CirclePackingConstants.c_n_two

by xuanji · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-packingdiscrete-geometry

c2=π(3−22)c_2=\pi(3-2\sqrt2) for the supremum-defined equal-disk packing constant in the unit square.

Preamble
import Definitions.Def_CirclePackingConstants

noncomputable section

namespace CirclePackingConstants
Formal statement
theorem c_n_two :
    c_n 2 = Real.pi * (3 - 2 * Real.sqrt 2) := by sorry
Source
User-supplied Circles in squares: proofs and bounds, p. 1, and accompanying CirclePacking.lean source package, supplied September 12, 2026.
Read-back

What the Lean code literally says, in plain math · gpt-6-astra

Let RR be the supremum of the set of real numbers rr such that 0≤r≤120\le r\le \tfrac12 and there exist two points (x0,y0),(x1,y1)∈R2(x_0,y_0),(x_1,y_1)\in\mathbb R^2 satisfying r≤xi≤1−rr\le x_i\le 1-r and r≤yi≤1−rr\le y_i\le 1-r for each i∈{0,1}i\in\{0,1\}, and (2r)2≤(x0−x1)2+(y0−y1)2(2r)^2\le (x_0-x_1)^2+(y_0-y_1)^2. Then 2πR2=π(3−22)2\pi R^2=\pi(3-2\sqrt2). The defining conditions allow equality at every boundary, and allow r=0r=0, in which case the two points may coincide.

Human review

  • Endorsed by Shuze Chen · Sep 12, 2026

  • Endorsed by xuanji · Sep 12, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph