The ambidextrous sofa

In 1966 Leo Moser asked for the largest sofa that can be carried round a right-angled corner in a hallway one unit wide.Moser’s Problem 66-11 in SIAM Review. “Sofa” means any connected shape in the plane, and only its area counts. The question sounds like a puzzle for an afternoon and has lasted sixty years. In 1992 Joseph Gerver found a shape of area 2.2195…, built from eighteen curves, and conjectured that nothing does better. In 2024 Jineon Baek announced a proof that Gerver was right, and the proof has since been formalised in the Lean proof assistant.

This piece is about a version that is still open. The sofa has to be able to take the corner in either direction: turning right, and also, from the same starting position, turning left. Dan Romik called such a shape an ambidextrous sofa. I proved that its area can be at most $353/200=1.765$, with a computer doing one large, carefully checked piece of the work. What follows is how that proof goes, with the figures doing their own geometry as you read, and in section 5 a smaller version of the computer’s part that your browser can check for itself.

The problem

Picture the hallway coming in from the left, and at the corner, a choice: it carries on downwards, or upwards. A shape starts in the horizontal arm, and has to be able to finish in the downward arm by one continuous motion, and in the upward arm by another. The two motions can be different, but they start from the same place.The common start matters. If each turn could begin from its own starting position, every shape that turns right would also turn left from some position, and the ambidextrous problem would be the ordinary one.

The largest such shape anyone knows was found numerically by Philip Gibbs in 2014, and worked out exactly by Romik in 2018. It is symmetric top to bottom, with a notch carved out of each long side by the inner corner of one of the two turns. Its area is

Nobody knows whether Romik’s shape is the best. Pinning down the largest possible area, written ${\mu }_{\mathrm{A}}$, is Problem 6.63 in the list that Georgiev, Gómez-Serrano, Tao and Wagner compiled while testing AlphaEvolve, and Problem C41b in the list of optimisation constants that Davis, Ivanisvili, Tao and others maintain.

What was known

Romik’s shape gives a lower bound: ${\mu }_{\mathrm{A}}\ge 1.64495$… Upper bounds were scarcer. An ambidextrous sofa is in particular an ordinary sofa, so every bound for the ordinary problem applies to it, but those bounds are about a shape that only has to turn one way, and they leave a wide gap. Kallus and Romik, who proved the bound 2.37 for the ordinary problem in 2018, pointed out the gap and called it “an appealing opportunity for further work”.

The paper proves two upper bounds. One, $2\text{√}2-1=1.8284$…, needs nothing but a careful argument and some areas worked out by hand. Vico Bonfioli announced the same bound earlier this year.Bonfioli’s note describes each turn by a rotation running from 0° to 90°, which takes for granted that the sofa passes through the orientation 45°. Section 4 below shows that every sofa of area more than $\text{√}2$ does. The other, 1.765, needs a computer. Both have been formalised in Lean, apart from one step: the run of the verified checker over a 1.74 GB certificate, which is done by compiled code.

Turning the problem inside out

The method comes from Kallus and Romik, and it starts with a change of viewpoint. Instead of watching the sofa move through the hallway, sit on the sofa and watch the hallway move around you. At every moment of the turn, the sofa lies inside the hallway. So in the sofa’s own frame, it lies inside every position the hallway takes.

Take a few of those positions: say one in which the hallway has turned 30°, one at 60°, and the strip the sofa started in. The sofa lies in all of them, so it lies in their intersection. That intersection may fall into several pieces, but the sofa is connected, so it sits inside just one. Its area is at most the area of the largest piece.

That bound depends on the motion, which we don’t know. So forget it: let each hallway slide to wherever it likes, independently of the others, and take the worst case, the largest piece over all positions. This is a number we can hope to compute, and it bounds the area of every sofa whose motion passes through those angles. For an ambidextrous sofa there are two families of hallways, the ones from the right turn and their mirror images from the left turn, and we can use some of each.

Try one hallway at 45°. Its two arms each cross the strip in a parallelogram of area $\text{√}2$, and with the corner placed just right the two parallelograms join, giving $2\text{√}2=2.83$. That is the first upper bound anyone proved for the ordinary problem, Hammersley’s from 1968, seen this way. Now add a mirrored hallway at 45°, as an ambidextrous sofa allows. Where an arm of one hallway crosses an arm of the other at right angles, they meet in a unit square tilted by 45°, and such a square meets the strip in area at most $\text{√}2-\frac{1}{2}$. In the best placement the intersection is exactly two such squares, touching at a single point: the total is $2\text{√}2-1$, exactly one less than Hammersley’s bound. No placement of the two hallways does better, which the paper proves by slicing the intersection into horizontal lines and adding up their lengths. Press climb from anywhere and the search will not get past 1.8284 either.

With more angles the bound improves. Romik’s own positions at two angles each way, about 36.87° and 53.13°, leave a connected region of area 1.7229, with Romik’s shape inside it, as it must be. But the hallways are free to move, and the best placement found by local search makes a piece of area 1.7317. Whatever bound we prove from these four hallways can never be smaller than that.

Why the sofa has to turn

There is a gap in the argument so far. To use a hallway rotated by 45°, we need to know that the sofa actually is rotated by 45° at some moment of its turn. For the ordinary problem, Kallus and Romik could rely on a theorem of Gerver: a sofa of the largest area can be moved with its rotation always increasing, so it passes through every angle on the way to 90°. Nothing like that is known for ambidextrous sofas. A priori a sofa might wobble, rotate the wrong way first, or turn round more than once.

The way round this is a variant of an argument of Gerver’s, in a form given by Baek, and it rests on one curious fact about hallways turned sideways. Suppose that at some moment the sofa has rotated by 45° against the direction of its turn. Then, seen from the sofa, the hallway’s corner points straight along the strip, and every horizontal line meets the hallway in a segment of length exactly $\text{√}2$.

The sofa lies both in the strip and in the hallway, so its area is at most $\text{√}2$. A sofa with more area than that can therefore never be at −45° (nor at 135°, the same position turned round), and since its rotation changes continuously and starts at 0°, it stays strictly between −45° and 135° throughout the right turn.

Now look at the end of the turn. The sofa finishes in the downward arm, a vertical strip of width 1. Seen from the sofa, that strip crosses the starting strip at an angle, and two strips of width 1 crossing at an angle $\phi$ share a parallelogram of area $1/|\sin \phi |$. A sofa of area $A$ must fit into it, so its final rotation is within $\arcsin (1/A)$ of a right angle, and the only right angle in the allowed range is 90° in the direction of the turn. Rotation changes continuously, so on the way the sofa passes through every angle from 0° to $90°-\arcsin (1/A)$. For an area of 1.765 that is everything up to about 55.5°, and both 45° and 53.13° are within reach. The same holds for the left turn, mirrored. Nothing about the motion is assumed except that it is continuous.The paper also treats a second formulation, in which the sofa passes through a Z-shaped corridor: a left turn followed, some distance $D$ further on, by a right turn. A short extra argument shows that for $D\ge 7$ a sofa of area more than $\text{√}2$ is too short to be in both corners at once, and the same bounds follow.

That settles the hand-made bound: every ambidextrous sofa of area more than $\text{√}2$ passes through 45° in both turns, so it lies in a configuration like the one in Figure 3, and its area is at most $2\text{√}2-1=1.8284$.

Handing it to a computer

To get further I used two angles each way, $\arcsin (3/5)\approx 36.87°$ and $\arcsin (4/5)\approx 53.13°$, the two acute angles of the 3–4–5 triangle. They were chosen for their sines and cosines, which are fractions, so that every corner of every polygon in the computation has rational coordinates and every area is an exact fraction. Nothing has to be rounded.

Four hallways, each placed by two numbers, make eight unknowns. A first lemma confines them: any connected piece of the intersection is at most 5 units long, so the whole search can be restricted to an explicit box in eight dimensions. The question becomes whether the largest piece ever exceeds 1.765 for any point of that box.

No computer can try every point, but it can try every box. Let each hallway range over a whole little box of positions at once. The union of all those hallways is again a simple shape: the hallway thickened along its two arms, still made of two convex pieces. Intersect the thickened hallways with the strip, and the largest piece of that is at least as large as anything any single point in the box could produce. If it is at most 1.765, the whole box is done. If not, cut the box in half along one coordinate and try each half.

The record of all those cuts is a binary tree, and the tree is the proof. Each internal node says which coordinate was halved; each leaf is a box whose bound came in at or under 1.765. Since the halves of a box cover it, the leaves cover the whole starting box, and the theorem follows. The tree is written as a string of digits and the letter L, one symbol per node, in order. For 1.765 it has 436,160,442 leaves, goes 71 cuts deep, and takes 1.74 GB.

Finding the tree and checking it are separate jobs. A search program, written for speed in floating-point arithmetic, decides where to cut, with a small safety margin. It can make mistakes, and it doesn’t matter if it does: a wrong decision can only produce a leaf whose bound is too large, or a tree of the wrong shape, and the checker will reject both. Only the checker has to be right, and it uses exact arithmetic throughout. It recomputes every box from the starting one, builds the polygons, adds their areas as fractions, and where the total is too large, works out which polygons touch, including polygons squashed flat to a segment or a point, which have no area but can still join two pieces.

1.765 is the smallest threshold I tried. Every step down makes the tree much bigger, because the boxes have to get small enough to separate configurations that come ever closer to the threshold, and below 1.7317 no tree exists at all.

Who checks the checker

The certificate was accepted by three checkers that share no code: one written in C with integer arithmetic, every operation checked for overflow; one in Python with exact fractions; and one written in Lean, the proof assistant, together with a proof that it is correct. The Lean checker is the one that matters most. The whole argument, from the definition of a sofa to the bound, is formalised in about 5,000 lines of Lean, and the final theorem says that if the checker returns true on any file whatsoever, the bound holds:

theorem ambidextrousSofaConstant_le_of_checkCert {T : ℚ} (hT : 5/3 ≤ T)
    {bytes : ByteArray} (h : checkCert T bytes = true) :
    ambidextrousSofaConstant ≤ ENNReal.ofReal T

The definitions of a sofa, a motion and the ambidextrous constant are copied unchanged from Google DeepMind’s Formal Conjectures project, where they were written independently, so the statement can be compared against someone else’s reading of the problem. What remains to trust is those definitions, Lean’s kernel and compiler, and the few unverified lines that read the file and print the answer. The certificate itself need not be trusted at all. On a desktop computer the Lean checker’s run took 13 minutes, the C checker’s 21 minutes, and the Python checker’s five and a half hours.

What is left

So the largest ambidextrous sofa has area somewhere between 1.64495 and 1.765. The method could squeeze a little more out of these four hallways, but not past 1.7317, and adding more angles makes the computation far more expensive: with three angles each way, local search finds configurations of about 1.7217, but the search for a certificate needed about six times as many boxes even at the easy threshold 1.85. Getting close to Romik’s shape will need better estimates on each box, or a way to use the problem’s symmetry to shrink the search.

Some questions this leaves open:

• Is Romik’s shape the largest? Is it at least better than every nearby ambidextrous sofa?
• With one hallway each way at an angle $a$, is the worst case always exactly $\sec a+\csc a-\csc 2a$? It is at 45°, where this gives $2\text{√}2-1$, and a numerical search at every 5° from 30° to 60° reached this value to ten digits without ever exceeding it.
• Kallus and Romik showed that the best ordinary sofa must rotate by at least 81.2°. Must a large ambidextrous sofa rotate much further than the 55° shown above?

@misc{okeefe2026sofa,
  author = {Devin O'Keefe},
  title  = {The ambidextrous sofa},
  year   = {2026},
  url    = {https://devinokeefe.com/ambidextrous-sofa/},
  note   = {Explainer for the paper Upper bounds for the ambidextrous moving sofa problem}
}