Moving Sofa Problem

Conjecture · volume_eq_sofaConstant_iff_congruent_gerversSofa

Gerver's sofa is the unique sofa that attains the sofa constant, up to a rigid motion.

The motion is needed: horizontalHallway is $(-\infty, 1] \times [0, 1]$ , so a leftward translate of any moving sofa is again one, obtained by sliding right and then following the original motion. It has the same area, so uniqueness cannot hold on the nose.

Formal statement · Lean 4.lean

theorem volume_eq_sofaConstant_iff_congruent_gerversSofa (s : Set ℝ²)
    (hs : ∃ m, IsMovingSofa s m) :
    volume s = sofaConstant ↔ ∃ g : E(2), s = g '' gerversSofa := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗