{"id":"palomar/PALOMAR-2026-10-13-000003","url":"https://github.com/vltanh/lean4-ambidextrous-sofa/tree/0f24fe48b4cadf02a442420e677b45a036136dbf","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000003-v1.json","repo":"https://github.com/vltanh/lean4-ambidextrous-sofa","tags":["math.MG","math.OC","msc:49Q10","msc:52A10","msc:52A38","msc:52A40","msc:68V20","computational-geometry","moving-sofa","lean"],"score":0,"title":"Optimality and uniqueness of Romik's ambidextrous sofa, formalized in Lean 4","trust":"high","domain":"math.MG","source":"palomar","authors":["The-Anh Vu-Le"],"reviews":0,"subject":"math.MG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-13","reactions":{},"formalized":true}