Optimality of Gerver's sofa

This repository contains a Lean 4 proof that Gerver's sofa has the largest area of any shape that can be moved around a right-angled corner in a hallway of width one. This is the moving sofa problem, solved by Jineon Baek in Optimality of Gerver's Sofa (2024).

theorem MovingSofa.sofaConstant_eq_volume_gerversSofa : sofaConstant = volume gerversSofa

• The statement is copied from Google DeepMind's formal-conjectures and passes comparator.
• The statement is formalized unconditionally: the Green-type curve area identity and the Minkowski-type mixed area facts that the paper quotes are proved here.
• The proof is about 66,000 lines of Lean, not counting dependencies. It was written in about four days by AI coding agents (OpenAI Codex and Claude Code), directed by Dean Cureton.

Built on

• Jineon Baek's paper: followed step by step
• GerverSofaLean by Dawid Trela: Gerver's four constants exist and are unique, and Gerver's sofa really does get around the corner. Vendored in vendor/gerver-sofa (v1.1.0, MIT, patched for current Mathlib)
• formal-conjectures: the formal statement (MovingSofa.lean)
• lean-pool: Jonathan Ho's Brunn–Minkowski (BrunnMinkowski.lean), vendored in vendor/lean-pool
• jordan_pick: the Jordan curve theorem (JordanCurve.lean)
• TauCeti: Jordan curves from two arcs (Path.lean), filled hulls (FilledHull.lean), bounded variation (BoundedVariation.lean, MetricVariation.lean), vendored in vendor/tauceti
• Mathlib

What's proved

The hallway is . A moving sofa is a nonempty closed connected set in the horizontal arm, plus a continuous family of rigid motions that starts at the identity, keeps the set inside the hallway, and ends with it in the vertical arm. sofaConstant is the supremum of the areas of moving sofas. The theorem above is Theorem 1.1 of the paper.

Comparator checks two more theorems:

• MovingSofa.GerversSofa.ABφθSpec.existsUnique: the four equations for Gerver's constants have exactly one solution; gerversSofa is defined from it
• MovingSofa.isMovingSofa_gerversSofa: Gerver's sofa is itself a moving sofa, so it attains the supremum

Two caveats: the statement fixes where the paper allows a translate (proved equivalent), and the area of Gerver's sofa is only shown to be ; the actual value isn't checked.

The proof

The proof follows the same route as the paper. Any sofa of area is dominated by a balanced maximum sofa with rotation angle , a limit of area-maximizing polygons. Its cap satisfies an injectivity condition, which lands it in a convex space of caps where area is bounded by a functional . Mamikon's theorem makes quadratic and concave, and the directional derivative of at Gerver's cap is in every direction, so Gerver's cap maximizes . There is exactly the area of Gerver's sofa. The bound for Gerver's sofa is an interval-arithmetic certificate checked by decide +kernel.

Formalizing the paper surfaced 11 small errors/gaps in the paper's proofs, and 33 misprints. These are all repaired here, and none of them break the main theorem. See NOTES.md for more details.

Build

lake exe cache get
lake build

Challenge.lean gives three expected sorry warnings. The build can be quite slow, in part due to the vendored certificate.

Comparator accepts the solution against comparator.json, including the nanoda kernel replay.

Licensed under Apache-2.0, vendor/gerver-sofa is MIT.