Prove2Me

Exact packing constant for n = 4

Proved
CirclePackingConstants.c_n_four

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

circle-packingdiscrete-geometry

Prove the exact optimum d₄ = 1, equivalently c₄ = π/4.

Preamble
import Definitions.Def_CirclePackingConstants

noncomputable section

namespace CirclePackingConstants
Formal statement
theorem c_n_four :
    c_n 4 = Real.pi / 4 := by sorry
Source
User-supplied Circles in squares: proofs and bounds, pp. 2–3, supplied September 12, 2026.
Read-back

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

Let RR be the supremum of all real numbers rr satisfying 0≤r≤1/20 \le r \le 1/2 for which there exist four indexed points pi=(xi,yi)p_i=(x_i,y_i) in the real plane such that r≤xi≤1−rr \le x_i \le 1-r and r≤yi≤1−rr \le y_i \le 1-r for every index ii, and (2r)2≤(xi−xj)2+(yi−yj)2(2r)^2 \le (x_i-x_j)^2+(y_i-y_j)^2 whenever i≠ji \ne j. Then 4πR2=π/44\pi R^2=\pi/4. The admissible radii include zero, at which the indexed points may coincide; all containment and separation inequalities allow equality.

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