Exact packing constants for two and three disks

Proved

CirclePackingConstants.c_n_two_and_three

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

circle-packingdiscrete-geometry

The conjunction of the exact formulas for $c_2$ and $c_3$ .

Preamble

import Definitions.Def_CirclePackingConstants

noncomputable section

namespace CirclePackingConstants

Formal statement

theorem c_n_two_and_three :
    c_n 2 = Real.pi * (3 - 2 * Real.sqrt 2) ∧
    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