What was already known
Baek’s 2024 paper established optimality. The project identifies uniqueness as a separate target and adds quantitative stability; the ambidextrous left-and-right-turning sofa problem is a different statement.
AI involvement
Vu-Le directed the project. ChatGPT Pro 6 produced the uniqueness, stability and coercive-certificate arguments; Claude Opus 5.5 completed and repaired their Lean proofs while retaining credited human prior work.
The contribution log credits models with the new uniqueness, stability and coercive-certificate mathematics, including model repairs; Baek’s earlier optimality remains prior human work.
Importance
Strengthens a known geometric optimum into uniqueness and a quantitative description of near-optimal shapes.
Limitations
The result uses the project’s continuous-motion definitions and its coercive certificate built from Baek’s framework. No human has reviewed the proof, statements or definitions according to the disclosure. This record concerns version 5’s ordinary moving-sofa results, not the already covered ambidextrous optimum. AIProofWatch has not rebuilt the formal development or audited the complete proof. Palomar reports mechanical checking of a pinned statement; its automated statement review is not human peer review. The reported date records this registry checkpoint; the earlier first-report date of the formalization has not been established.
Technical verification
A completed rigorous check is documented for the scoped statement. Palomar: Lean, NanoDa and con-ron (reported): Baek.gerver_sofa_unique, gerver_sofa_stable, gerver_sofa_stability_exponent and the recorded bridge/certificate declarations in version 5 at 1174c5c25c1c66b807e368446d6682e8d0276759; three standard Lean axioms.
Formal checking
Registry-reported Comparator and kernel checking; not reproduced by AIProofWatch.
- Checker
- Palomar: Lean, NanoDa and con-ron (reported)
- Scope
- Baek.gerver_sofa_unique, gerver_sofa_stable, gerver_sofa_stability_exponent and the recorded bridge/certificate declarations in version 5 at 1174c5c25c1c66b807e368446d6682e8d0276759; three standard Lean axioms.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-07
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. No sufficient account of a named human explaining the scoped central reasoning is established in this assessment. Missing disclosure is not evidence of little understanding.
Correction and publication history
Source-statement, baseline, AI-role and verification-scope review, 14 October 2026. New curated contribution; eligible for matching consented digests.
Read this published revision