Wikipedia · textbook · AMS 49

mediumknown result, no worker yet

Moving Sofa Problem

Theorem · ABφθSpec.existsUnique

There exist unique constants AA, BB, φ\varphi, and θ\theta satisfying the spec.

Formal statement · Lean 4.lean
theorem ABφθSpec.existsUnique : ∃! ABφθ : ℝ × ℝ × ℝ × ℝ,
    ABφθSpec ABφθ.1 ABφθ.2.1 ABφθ.2.2.1 ABφθ.2.2.2 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗