The Carathéodory Conjecture on Umbilic Points
Carathéodory's conjecture, Problem 8.1 of Ghomi's list and traceable to 1922, asks whether every closed convex surface in has at least two umbilic points. Hamburger settled the real-analytic case in 1940-41 and it stands. The case is false: an explicit support function gives a smoothly embedded two-sphere bounding a convex body with exactly one umbilic point. The same family disproves the smooth Loewner conjecture, whose member at has an isolated trace-free Hessian zero of winding number three.
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-assisted
- Method
- Construction
- Field
- Differential geometry
- Posed by
- Constantin Carathéodory
- Year posed
- 1922
- Years open
- 104y
- Solved
- 2026-08-19
- Model
- Claude, Codex
- Vendor
- Anthropic, OpenAI
- Collaborators
- Levent Alpöge, John-Paul Smith
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 55 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Only the smooth case falls. Hamburger's real-analytic theorem is untouched, and the counterexample is explicitly a object, so the conjecture's classical analytic form remains true. The gap between the two is the whole content of the result.
What the AI did
Two distinct roles, neither of them the discovery. The formalization's module docstring records that Alpöge's announcement "credits John-Paul Smith and Claude with checking the construction", so the model's part was verifying a human construction. Separately, the Lean development was, in its author's words, "developed with Codex and parallel proof-review agents" - a formalization of a human result, which the methodology does not count as the contribution. Recorded as assisted rather than co-developed for that reason; the submission proposed co-developed.
Verification
Audited by this site on 21 August 2026 at the commit the formal_proof attribute pins (7aa855b, google-deepmind/formal-conjectures). The formalized hypothesis is the classical statement and not a weakened one: IsConvexSphereOfClass requires Topology.IsEmbedding together with range F = frontier K for a compact convex K of nonempty interior, so "parametrized" names the Gauss parametrization rather than admitting mere immersions. The pinned line is not_caratheodoryConjectureOfClass_infty, the smooth statement, and the proof tree is 8013 lines carrying zero sorry, zero declared axioms and no native_decide. Not lean-verified, because that commit is NOT merged - it is diverged from main by 11 commits and behind by 26, and both upstream pull requests are drafts, #5070 saying "I'm currently checking this ... please ignore". The Lean was read here, not compiled, and the announcement itself is an X post.
Sources
- PaperThe informal proof accompanying the formalization
- Lean proofLean proof, sorry-free at the pinned commit
- Lean statementLean statement of the smooth and analytic conjectures
- AnnouncementLevent Alpöge, X announcement of the smooth counterexample
- Problem recordGhomi, Open Problems in Geometry of Curves and Surfaces (Problem 8.1)
Submitted by VelvetFalcon287 on