Optimality and uniqueness of Romik's ambidextrous sofa, formalized in Lean 4
The ambidextrous moving sofa problem asks for the largest area of a connected planar shape that can be moved, from one starting position, around the right-angled corner of a hallway of unit width that turns right, and also around the corner of a hallway that turns left. Dan Romik (Experimental Mathematics, 2018) constructed a shape of area M = 1 + 4Y^2 + arctan Y = 1.64495..., where Y = 0.2980... is the positive root of 4Y^3 + 3Y = 1, and proposed it as a likely solution; in 2025 Georgiev, Gómez-Serrano, Tao and Wagner listed the problem as open. This entry proves that Romik's ambidextrous…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-13-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-13-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'