Optimality and uniqueness of Gerver's sofa in Lean 4

Anyone who has moved a couch knows the moment when the hallway turns a corner and the couch has to pivot to get around it. Leo Moser turned this into a mathematical question in 1966. A moving sofa is a connected shape in the plane that can be moved, by sliding and turning, through a hallway of width \(1\) with a right-angled corner. How large can its area be?

Gerver's sofa slides along the horizontal side of an L-shaped hallway of unit width, turns the corner, and leaves along the vertical side — Gerver's sofa going around the corner. The animation is computed from the same definitions as the proofs.

The largest shape known is Gerver’s sofa, the one above, found by Joseph Gerver in 1992. Its area is \(2.2195\ldots\) and its boundary is made of 18 pieces of curves. In 2024, Jineon Baek proved that no moving sofa is larger. This project checks that proof in Lean 4 and adds two results of its own:

Optimality: Baek’s whole proof, 119 pages long, is formalized, together with the results it takes from the literature and a theorem on the structure of Gerver’s sofa that the paper states without proof.
Uniqueness: every moving sofa of maximum area is Gerver’s sofa, after a rotation and a translation. Baek’s paper does not prove this, and Google DeepMind’s formal-conjectures lists it as an open problem. As far as I know, this is its first proof.
A bridge to formal-conjectures, which states the problem with definitions of its own: the project proves that these describe the same sofas, the same maximum area and the same Gerver’s sofa as Baek’s, so the statements of formal-conjectures, the open one included, follow.

Why it’s hard

A moving sofa is any connected shape that has some motion through the hallway, so the problem optimizes over infinitely many shapes and motions at once. For a long time nobody could write down the area of a general sofa. Every derivation of Gerver’s sofa assumed its shape in advance and showed that small changes don’t increase its area, which only shows that it is a local maximum.

Baek’s proof gets around this with an upper bound. For a well-behaved sofa it builds a larger region whose area \(\mathcal{Q}\) can be computed, and that bound is a concave function of the sofa. A concave function’s local maximum is a global one, and Gerver’s sofa is a local maximum of \(\mathcal{Q}\), where the bound equals the area. Most of the paper shows that a largest sofa is well behaved enough for the bound to apply.

Prior work

Hammersley found a sofa of area \(\pi/2 + 2/\pi \approx 2.2074\) in 1968 and showed that no sofa is larger than \(2\sqrt2\). Gerver found his sofa in 1992 and conjectured that it is optimal. Dan Romik derived it from a system of differential equations in 2018 and found its exact description; Kallus and Romik proved by computer that no sofa has area above \(2.37\). Baek’s preprint closed the gap in 2024.

Two other Lean formalizations of Baek’s proof appeared shortly before this one, by Dean Cureton and by Ruifeng Cao. Both prove formal-conjectures’ statement that Gerver’s sofa has the maximum area. This one states the theorem with Baek’s own definitions, proves uniqueness, and checks the paper itself: the repository’s report lists the statements that needed a correction. Each has an evident fix, and every result of the paper holds.

The proof

Baek’s proof narrows down what a largest sofa can look like until the upper bound applies.

Gerver's sofa between the lines y=0 and y=1, with the arch of its niche traced by the inner corner of the moving hallway — Gerver's sofa, seen from the sofa as the hallway moves around it. The inner corner of the hallway traces the arch underneath (orange), its rotation path.

Seen from the sofa, the hallway rotates and slides around it, and the sofa fits inside every position of the hallway. A largest sofa can be taken to be monotone: the intersection of the hallways that touch it from outside. Such a sofa is a convex cap minus the niche carved out by the inner corner, so the problem becomes one about convex bodies.

Next, a largest sofa is a limit of polygons whose opposite sides balance in length. The idea is Gerver’s, and Baek repairs it, because Gerver’s argument could disconnect the sofa. Balance gives room for a full right-angle turn, and a differential inequality on the balanced sides then shows that the corner’s path, the arch above, never loops back.

For such sofas, Baek encloses the sofa in a region shaped like Gerver’s sofa, whose area \(\mathcal{Q}\) is a quadratic function of three convex bodies. Mamikon’s theorem on swept areas makes it concave, and Romik’s differential equations show that no direction increases it at Gerver’s sofa, which is therefore its maximum.

Uniqueness

Baek’s argument proves the needed properties only for one particular largest sofa, a limit of polygons chosen by compactness, so optimality alone does not give uniqueness. The uniqueness proof redoes those steps for any largest sofa. It approximates the given sofa’s cap by polygons that maximize area minus a penalty for straying from it, and passes the polygons’ balance conditions to the limit as curvature bounds. These give the given sofa the right-angle turn and the non-looping corner path, so Baek’s bound applies to it. Equality in the bound then forces equality in each of Mamikon’s swept areas, which pins the cap down to Gerver’s, up to a horizontal shift. Finally, Gerver’s sofa is the closure of its interior, so a closed set inside it with the same area is all of it. ChatGPT Pro 6 found this argument. It has not been peer reviewed; Lean checks every step of the formal proof.

Verification

Lean checks every proof, assuming nothing beyond its three standard axioms. The theorems are restated in a self-contained file, with copies of the definitions in Mathlib’s vocabulary, and Comparator checks that the proofs prove exactly those statements. The project is registered in the Palomar registry as PALOMAR-2026-10-02-000008, whose check also replays the proofs through the NanoDa and con-ron kernels. The proofs are written out in docs/proof/, an illustrated textbook in which every result links to the Lean code that proves it.

Follow-up

The ambidextrous sofa project uses this formalization of Baek’s theorem to prove that Romik’s ambidextrous sofa, which turns both right and left, is the largest sofa of its kind.

Contributors

Claude Opus 5.5 formalized Baek’s paper, wrote the audit of the paper, and completed the uniqueness proof and the bridge from Lean drafts by ChatGPT Pro 6, which also wrote the uniqueness argument. I directed the work. The agents followed my skill for formalizing papers, formalize-math-paper. The repository’s contributors page records who did what, and how long each part took.

References

L. Moser, Problem 66-11, Moving furniture through a hallway, SIAM Review 8 (1966), 381.
J. L. Gerver, On moving a sofa around a corner, Geometriae Dedicata 42 (1992), 267–283.
D. Romik, Differential equations and exact solutions in the moving sofa problem, Experimental Mathematics 27 (2018), 316–330.
Y. Kallus, D. Romik, Improved upper bounds in the moving sofa problem, Advances in Mathematics 340 (2018), 960–982.
J. Baek, Optimality of Gerver’s sofa, arXiv:2411.19826 (2024).