The moving sofa problem asks for the planar shape of largest area that can be moved around the right-angled corner of a hallway of unit width. Jineon Baek, Optimality of Gerver's Sofa (arXiv:2411.19826v1), proves that Gerver's sofa, of area 2.21953…, is optimal. This repository proves in Lean 4 with Mathlib:

• optimality: Baek's whole proof, with the results it takes from the literature, and the structure of Gerver's sofa (Theorem 8.4.1), which the paper states without proof;
• uniqueness: every moving sofa with the area of Gerver's sofa is congruent to it. So Gerver's sofa is, up to rigid motions, the only moving sofa of maximum area. Baek's paper does not prove this, and Google DeepMind's formal-conjectures lists it as an open problem. The argument was written by ChatGPT Pro 6 (OpenAI) for this repository and has not been peer reviewed; Lean's kernel checks every step of the formal proof.

Challenge.lean states the main results of the first two parts in Mathlib's vocabulary, and Solution.lean proves them.

• All numbered results of the paper (Chapters 1–8), proved along the paper's arguments, and the main theorem, Theorem 1.1.1 (theorem1_1_1). Where the paper's statements contain slips, the intended statements are proved. REPORT.md lists every correction; no result had to be weakened.
• The cited results used in proofs:
  • Schneider's area formula |K| = ½ ∫ h_K dσ_K for planar convex bodies (area_eq_half_integral_supp, in MovingSofaOptimality/External/);
  • the existence and uniqueness of the solution of Romik's system of equations that defines Gerver's sofa (GerverParams.romik_exists, GerverParams.romik_unique, also in MovingSofaOptimality/External/);
  • the facts the paper cites from convex geometry and measure theory, which are proved where they are used or come from Mathlib.
• The structure of Gerver's sofa (Theorem 8.4.1, and with it Theorems 6.1.2 and 8.4.2), and its area, between 2.2192 and 2.2199, proved from Romik's equations by rigorous interval arithmetic.

• The theorem: a moving sofa whose area equals that of Gerver's sofa is mapped onto Gerver's sofa, as a set, by a rotation about the origin followed by a translation (image_eq_gerver_of_volume_eq).
• Equivalent forms: a moving sofa has the area of Gerver's sofa if and only if a rigid motion maps it onto Gerver's sofa (volume_eq_gerver_iff); the moving sofas of maximum area are exactly the moving sofas that a rigid motion maps onto Gerver's sofa (isGlobalMax_iff); a maximum exists and any two are congruent (globalMax_congruent, exists_globalMax_unique_up_to_rigid).
• The proof monotonizes the sofa, extends its motion to a right angle, shows that the cap of the resulting sofa satisfies Baek's injectivity condition, and then uses the equality case of Baek's upper bound to identify it with Gerver's cap; regular closedness of Gerver's sofa recovers the original set. docs/UNIQUENESS.md maps each step of the informal proof, note 20, to Lean.

lake build succeeds, and the only sorrys are the five statements of Challenge.lean. There are no axioms, and scripts/Audit.lean checks that every declaration of both libraries uses only propext, Classical.choice and Quot.sound. Run it with lake env lean scripts/Audit.lean; it also prints, for each result of the paper and each step of the uniqueness proof, the results from prior work that its proof uses.

Challenge.lean states the results in Mathlib's vocabulary only, with its own copies of the definitions (the hallway, moving sofas, Romik's parameters and Gerver's sofa), so that it can be read without the rest of the repository. Solution.lean proves them from the two libraries.

• gerver_params_exists and gerver_params_unique: Romik's system of equations (27)–(44) has exactly one solution with φ ∈ [0.039, 0.04] and θ ∈ [0.68, 0.69]. So Gerver's sofa, the shape of the rotation path these parameters define, is well defined.
• gerver_sofa_area: Gerver's sofa has area between 2.2192 and 2.2199. Gerver's value is 2.21953…; this ties the shape defined from Romik's parameters to the sofa Gerver found.
• gerver_sofa_optimal: Gerver's sofa is a moving sofa, and every moving sofa has area at most the area of Gerver's sofa (Baek's Theorem 1.1.1).
• gerver_sofa_unique: every moving sofa with the area of Gerver's sofa is mapped onto Gerver's sofa by a rotation about the origin followed by a translation.

comparator.json configures Lake's Comparator, which checks in a sandbox that Solution.lean proves exactly the statements of Challenge.lean with the standard axioms only:

lake env lake comparator --config=comparator.json

The repository is packaged for the Palomar registry of machine-checked proofs. Version 1 of its entry, PALOMAR-2026-10-02-000008, registers the optimality part (commit d0b42d2).

• Challenge.lean holds the statements of record;
• Solution.lean holds their proofs;
• comparator.json, the only Comparator configuration, selects the five compared theorems;
• formalization.yaml records the metadata: sources, scope, divergences from the paper, automation and review;
• LICENSE holds the licence.

The workflow .github/workflows/palomar_preflight.yml runs Palomar's complete mechanical verification on a commit, on demand. It is pinned to a fixed commit of PalomarSubmission. Run it with gh workflow run palomar_preflight.yml --ref main; it publishes its report as the artifact mechanical-report-preflight001. The preflight does not cover the rendering of the Challenge, which Palomar runs after verification; see Building for the Mathlib pin that rendering needs.

• Leo Moser posed the problem in 1966 (SIAM Review 8, Problem 66-11).
• Hammersley found a sofa of area π/2 + 2/π ≈ 2.2074 and showed that the maximum is at most 2√2 ≈ 2.83.
• Gerver (Geometriae Dedicata 42, 1992) found a sofa of area 2.21953… and conjectured that it is optimal.
• Romik (Experimental Mathematics 27, 2018) derived Gerver's sofa from a system of differential equations and solved it explicitly; the Challenge's definition of Gerver's sofa follows him.
• Kallus and Romik (Advances in Mathematics 340, 2018) proved by computer that the maximum is at most 2.37.
• Baek's preprint (arXiv:2411.19826, 2024) proves that Gerver's sofa is optimal. This repository formalizes version 1 of it.
• That Gerver's sofa is the only optimal sofa, up to rigid motions, is not proved in Baek's paper. formal-conjectures states it as volume_eq_sofaConstant_iff_congruent_gerversSofa, in its category research open. We know of no earlier proof, but have not searched the literature systematically.

Two Lean 4 formalizations of Baek's proof appeared shortly before this one: deancureton/MovingSofa, written by AI coding agents directed by Dean Cureton, and RuifengCao/sofa-formal. Both prove the statement of Google DeepMind's formal-conjectures, sofaConstant = volume gerversSofa, and their READMEs report that Comparator accepts the proofs with only the standard axioms. The three differ as follows. The other two columns describe commits 4d55691 (2026-09-21) and ca8585c (2026-09-24), from their READMEs and sources.

Like the earlier two, this repository proves the facts about Gerver's sofa that the paper states without proof or takes from Gerver and Romik (Theorems 6.1.2, 8.4.1 and 8.4.2). For the niche, Theorem 8.4.1(2), the proof reduces a two-parameter family of inequalities to one-variable inequalities verified by interval arithmetic.

REPORT.md audits Baek's paper against its LaTeX source and the formalization. In short:

• Errors.
  • Definition 3.2.5 uses the parallelogram P_ω where the fan F_ω is meant, which makes Proposition 3.3.5 and Lemma 3.4.2 false as written (E6).
  • The direction (1) ⇒ (2) of Proposition 5.1.4 is false: an absolutely continuous function need not have a bounded density (E11).
  • Several statements have slips that make them false as printed, for example Lemma 8.3.6 (3), whose left side is identically 0 (E22), and Proposition 8.4.4 (4), shifted by π/2 (E25).
  • All results survive in their intended form.
• Gaps.
  • Theorem 8.4.1 has no proof (E23).
  • The proof of Theorem 6.1.2 misreads Gerver's Theorem 2 (E12).
  • The proofs of Lemma 8.1.7 and Theorem 8.2.4 use 𝒩(K) ⊆ K, which the cap space 𝒦^i does not give; the statements hold anyway (E20).
  • These gaps are filled here, and the remaining gaps are minor.
• Missing hypotheses: none.
• Redundant hypotheses: several, listed in Section 5 of the report; the Lean statements omit them.
• Use of cited results: correct, except for Gerver's Theorem 2 (E12). Romik's assertion that the solution of his system is unique is used by the paper without proof and is proved here.

For the uniqueness proof, docs/UNIQUENESS.md records how the formal proof follows the informal one and where it departs from it. The formalization found no gap in the argument. It found five helper lemmas of the Lean draft that were false as written, because hypotheses declared as section variables were not part of their statements; they are corrected.

The-Anh Vu-Le is the author and maintainer of this repository. AI systems wrote the code, the proofs and the documents at his request. No human has reviewed the proofs; Lean's kernel checks every one of them.

The statements, the proofs, the numerical verification scripts and the audit were written by Claude Opus 5.5 (Anthropic, model claude-opus-5-5), running in Claude Code 2.1.285.

• Procedure. The work followed the formalize-math-paper skill (commit cbdedac): state every result first, then prove the paper's results and the results it cites, verify, clean up, and audit the paper.

• Agents. One coordinating agent and 19 sub-agents, at most 13 of them running at the same time:

  • 17 proved groups of files, each a chapter or part of one, and for Gerver's sofa its separate components (Romik's system, the structure of the sofa, the niche, the area);
  • one reviewed every statement against the paper's LaTeX source before any proof was written;
  • one checked every finding about the paper against the LaTeX source for the audit.

  The coordinating agent wrote the statements, divided the work, checked and integrated every result, and wrote the documents. It also resumed finished sub-agents three times for follow-up work.

• Time. About 3 hours 50 minutes of elapsed time, from 2026-10-01 22:38 to 2026-10-02 02:28 (US Central Time), up to the audited formalization (commit 59b35c2). The sub-agents worked about 18 hours in total. All agents together made 3,135 tool calls (2,704 of them by sub-agents), generated 7.5 million output tokens and read 21 million input tokens, plus 1.2 billion tokens from the prompt cache. Preparing the Palomar submission came afterwards.

• The argument and the Lean draft. ChatGPT Pro 6 (OpenAI) wrote the informal proof (note 20 and the notes before it) and a Lean draft of it, without a compiler, in 147 commits from 2026-10-02 15:01 to 22:39 (US Central Time), in pull request #1 of this repository. Its effort was not recorded.
• The compiled proof. Claude Opus 5.5 (model claude-opus-5-5), running in Claude Code 2.1.287, with the same skill (version 1.3.0), made the draft compile and completed it:
  • It checked every module of the draft and replaced the 54 proofs that did not compile by sorry; every statement compiled.
  • Eight sub-agents, each owning a group of files, proved those 54 again, starting from the draft's proofs; a ninth reviewed the statements against note 20. At most nine ran at the same time.
  • The coordinating agent integrated the proofs, removed unused hypotheses, added the equivalent forms of the theorem and its statement in the Challenge, reorganized the repository into its three parts, and wrote the documents.
• Time. About 1 hour of elapsed time, from 2026-10-02 21:55 to 22:56 (US Central Time), up to the documented proof (commit 7f967fd); every proof compiled after 27 minutes. The sub-agents worked about 0.9 hours in total. All agents together made 607 tool calls (400 of them by sub-agents), generated 0.5 million output tokens and read 1.7 million input tokens, plus 105 million tokens from the prompt cache.

lake exe cache get        # download Mathlib's compiled files
lake build                # builds both libraries, Challenge and Solution
lake env lean scripts/Audit.lean

The toolchain is leanprover/lean4:v4.35.0-rc3 (lean-toolchain), and Mathlib is pinned to its release tag v4.35.0-rc3, with the exact revision in lake-manifest.json. Keep Mathlib on the release tag that matches the toolchain: Palomar renders the Challenge with Verso's release for the same toolchain, and the render fails when a package that Mathlib and Verso share, such as plausible, is pinned at two different revisions, as it soon is on Mathlib master.

Two Lean files are generated by scripts, which reproduce them exactly:

• MovingSofaOptimality/External/Romik/Num.lean: python3 scripts/romik/mk_num.py;
• MovingSofaOptimality/Gerver/AreaBounds.lean: cd scripts/area && python3 gen.py emit ../../MovingSofaOptimality/Gerver/AreaBounds.lean.

Both need Python 3 with SymPy and mpmath.

After changing the code, update the links from the documents to the code with python3 scripts/linkify_docs.py, which reads the .ilean files that lake build writes. Check the Markdown tables with python3 scripts/check_md_tables.py README.md REPORT.md docs/UNIQUENESS.md.

.github/workflows/lean_action_ci.yml builds the project on every push and pull request, runs the axiom audit, and checks that the documentation's links and tables are current. It needs no settings.

Apache-2.0 (LICENSE).