Gerver's sofa attains the maximum area of a moving sofa
OpenGerver.gerver_optimalThe moving sofa problem is resolved: Gerver's sofa attains the maximum area of any moving sofa. Some sofa satisfying the Gerver construction — the monotone sofa of a rotation path carried by the five boundary curves solving Gerver's balancing ODEs — has area at least that of every shape that can be moved around the corner of the unit-width L-shaped hallway. This is Theorem 1.1.1 of the source, the mission's goal.
import Mathlib import Definitions.Def_Gerver_arena import Definitions.Def_Gerver_monotone import Definitions.Def_Gerver_sofa
namespace Gerver
/-- Theorem 1.1.1 — the moving sofa problem: Gerver's sofa attains the maximum
area α_max of a moving sofa. Some sofa satisfying the Gerver construction —
the monotone sofa of a rotation path carried by the five boundary curves
solving Gerver's balancing ODEs — has area at least that of every moving
sofa. -/
theorem gerver_optimal :
∃ G, IsGerverSofa G ∧ ∀ S, IsMovingSofa S → area S ≤ area G := by
sorry
end Gerver
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: there exists a planar set G satisfying the Gerver sofa structure such that for every planar set S, if S is a moving sofa — a nonempty, compact, connected shape movable around the corner through a continuous path of orientation-preserving rigid motions — then the area of S is at most the area of G.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.