Moving Sofa Problem

Read formalization.yaml

authors

Dean Cureton

method

agent

review

agent-reviewed (Codex and Claude subagent reviewers (mathematical review of each proof, and statement checks against the paper), Claude subagent auditors (final audit, statement audit, whole-paper scope audit))

axioms

Classical.choice, Quot.sound, propext

sorry

0 unproved goals declared

sources

Optimality of Gerver's Sofa — formalizes, authors not-contacted; On moving a sofa around a corner — adapts, authors not-contacted; Differential equations and exact solutions in the moving sofa problem — background, authors not-contacted

related

google-deepmind/formal-conjectures/tree/ddfbaf90f4482030d88aae5233fe933874296a23 — adapts; dawidmtrela-dotcom/GerverSofaLean/releases/tag/v1.1.0 — builds-on; rkirov/jordan_pick/tree/b3c9b7cf7358bf81a077d78ad67e6e8247869ddd — builds-on; Vilin97/lean-pool/tree/bb74ee07fc23bc81358d75a9c40303e5e27fced8 — builds-on

divergences

Compared with formal-conjectures: MovingSofaSubmission/Challenge.lean copies the formal-conjectures definitions and both statements unchanged and imports only Mathlib. It inlines the plane notation and instances, names the rigid-motion topology instance so that Comparator sees the same name in Challenge and Solution, and leaves out the tests, metadata and open shape-uniqueness conjecture found there. Compared with the paper: an AI review of the statement found the following differences, none of which weakens the theorem. Sofas satisfy m 0 = id and start inside the horizontal arm, where the paper allows any initial translation; canonical_paper_motion_bridge proves that a sofa of either kind is a translate of one of the other kind. Sofas are closed and connected, as in the paper's Definition 1.2, so the theorem says nothing about disconnected sets. Motions lie in the full isometry group E(2), where the paper uses SE(2); orientation preservation is proved. Boundedness and measurability are not assumed; every moving sofa is proved compact. The supremum is taken in the extended nonnegative reals and is proved finite, at least 11/5 and attained. ABφθSpec uses non-strict inequalities, whi

checked by

nobody independent of its authors yet