All currently formalized exact circle-packing constants

Open

CirclePackingConstants.c_all

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

circle-packingdiscrete-geometry

The conjunction of all eleven exact covered-area formulas currently represented by the mission milestones: the constants $c_n$ for $n=2,3,4,5,6,7,8,9,16,25,36$ .

Preamble

import Definitions.Def_CirclePackingConstants

noncomputable section

namespace CirclePackingConstants

Formal statement

theorem c_all :
    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 ∧
    c_n 4 = Real.pi / 4 ∧
    c_n 5 = 5 * Real.pi *
      (((1 / Real.sqrt 2) / (2 * (1 + 1 / Real.sqrt 2)))) ^ 2 ∧
    c_n 6 = 6 * Real.pi *
      (((Real.sqrt 13 / 6) / (2 * (1 + Real.sqrt 13 / 6)))) ^ 2 ∧
    c_n 7 = 7 * Real.pi *
      (((4 - 2 * Real.sqrt 3) / (2 * (1 + (4 - 2 * Real.sqrt 3))))) ^ 2 ∧
    c_n 8 = 8 * Real.pi *
      (((Real.sqrt (2 - Real.sqrt 3)) /
        (2 * (1 + Real.sqrt (2 - Real.sqrt 3))))) ^ 2 ∧
    c_n 9 = Real.pi / 4 ∧
    c_n 16 = Real.pi / 4 ∧
    c_n 25 = Real.pi / 4 ∧
    c_n 36 = Real.pi / 4 := by sorry

Source

Aggregate of the eleven source-backed exact-value milestones in the Circle packing in a square mission, current September 12, 2026.

View graph