Optimality and uniqueness of the ambidextrous sofa
Follow the latest progress by email.
What is the largest area of a compact connected planar shape that can move continuously through both left- and right-turning unit-width corridors from the same initial orientation? Romik’s sofa is the candidate for this ambidextrous motion model.
Why it matters and what counts as progress
Why it matters: A shape that negotiates both turns obeys a different optimization constraint from the ordinary moving-sofa problem.
What counts as progress: Prove an upper bound matching the candidate’s area, determine all equality cases, or construct a larger admissible shape.
How the problem developed
- 2016 · Candidate [1]
Dan Romik Derived a closed-form ambidextrous sofa of area about 1.644955 and proposed it as the largest possible; optimality was not proved.
The-Anh Vu-Le; ChatGPT Pro 6 The project reports a Lean proof that Romik’s sofa is optimal and unique up to rigid motions for compact connected shapes that negotiate both turns from the same starting orientation.
AI contributions 2
ChatGPT-led proof establishes optimality and uniqueness of Romik’s ambidextrous sofa
Every compact connected planar set that can be moved continuously through both a right-turning and left-turning unit-width hallway from the same starting orientation has area at most M=1+4Y²+arctan(Y), where Y>0 solves 4Y³+3Y=1. Equality holds exactly for rotated and translated copies of Romik’s sofa, and the sofa attains M.
Vu-Le reports: optimality and uniqueness of the ambidextrous sofa
Vu-Le reports that every compact connected planar shape movable through both left- and right-turning unit corridors from the same initial orientation has area at most 1.64495…; equality identifies Romik’s sofa up to rigid motion.
Sources
- Dan Romik, Differential equations and exact solutions in the moving sofa problem (2016; published 2018)
- Pinned original statement and proof outline
- Original manuscript sources
- Completed Lean proof
- Proof checking record
- Documented AI and human roles
- Prior-work and ordinary-sofa distinctions
- Immutable registration and checking scope
Website timeline
Publication dates and editorial changes.
ChatGPT-led proof establishes optimality and uniqueness of Romik’s ambidextrous sofa
Vu-Le reports: optimality and uniqueness of the ambidextrous sofa