Prove2Me

Exact three-disk packing constant

Proved
CirclePackingConstants.c_n_three

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

circle-packingdiscrete-geometry

c3=3π(6−22(1+6−2))2c_3=3\pi\left(\frac{\sqrt6-\sqrt2}{2(1+\sqrt6-\sqrt2)}\right)^2 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_three :
    c_n 3 = 3 * Real.pi *
      ((Real.sqrt 6 - Real.sqrt 2) /
        (2 * (1 + (Real.sqrt 6 - Real.sqrt 2)))) ^ 2 := by sorry
Source
User-supplied Circles in squares: proofs and bounds, p. 1, and accompanying CirclePacking.lean source package, supplied September 12, 2026.
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