Optimality of Gerver's sofa

Source: arxiv:2411.19826, url:https://github.com/deancureton/MovingSofa/tree/4d5569131940815f47a9ccf3e90a4c5043c56127 Authors: Dean Cureton, Dawid Trela, Rado Kirov, Kirill Alkhimov Status: verified Main declarations: MovingSofa.sofaConstant_eq_volume_gerversSofa Tags: convex-geometry, moving-sofa-problem, geometric-optimization, interval-arithmetic MSC: 52A40, 52A10, 49Q10

Imported sources and provenance

The main formalization is from Dean Cureton's deancureton/MovingSofa at 4d5569131940815f47a9ccf3e90a4c5043c56127 (Apache-2.0). The proofs were produced using Codex and Claude Code under Cureton's direction. Completion was announced on 20 September 2026.

The coherent dependency closure also contains:

• Dawid Trela's dawidmtrela-dotcom/GerverSofaLean, release v1.1.0 (MIT; notice below), including its Part F bridge.
• alerad/leancert at 571a228555ae38742448854be81d7b59d994a8e3 (Apache-2.0): pure interval arithmetic and its soundness proofs, without the metaprogramming front end.
• Rado Kirov's rkirov/jordan_pick at b3c9b7cf7358bf81a077d78ad67e6e8247869ddd (Apache-2.0): Jordan separation and Brouwer.
• The Tau Ceti contributors: TauCetiProject/TauCeti at c52a81811e4626d2e9769fe9b0c701168c211332 (Apache-2.0): variation, filled hulls, and supporting topology.
• The Formal Conjectures Authors: google-deepmind/formal-conjectures at ddfbaf90f4482030d88aae5233fe933874296a23 (Apache-2.0): the moving-sofa definitions, with its open parameter theorem proved here.

Jonathan Ho's isoperimetric infrastructure is reused from LeanPool.Isoperimetric.