Prove2Me

Exact packing constant for n = 7

Proved
CirclePackingConstants.c_n_seven

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

circle-packingdiscrete-geometry

Prove the exact optimum d₇ = 4 − 2√3 and convert it to the corresponding exact value of c₇.

Preamble
import Definitions.Def_CirclePackingConstants

noncomputable section

namespace CirclePackingConstants
Formal statement
theorem c_n_seven :
    c_n 7 = 7 * Real.pi *
      (((4 - 2 * Real.sqrt 3) / (2 * (1 + (4 - 2 * Real.sqrt 3))))) ^ 2 := by sorry
Source
User-supplied Circles in squares: proofs and bounds, pp. 2–3, 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