The $C^\infty$ Carathéodory Conjecture on Umbilic Points
candidateconfidence 50%
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Carathéodory's conjecture, Problem 8.1 of Ghomi's list and traceable to 1922, asks whether every closed convex surface in $\mathbb{R}^3$ has at least two umbilic points. Hamburger settled the real-analytic case in 1940-41 and it stands. The $C^\infty$ 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 $k=1$ has an isolated trace-free Hessian zero of winding number three.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
Claude, Codex
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.
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.
Levent Alpöge, X announcement of the smooth counterexample
Only the smooth case falls. Hamburger's real-analytic theorem is untouched, and the counterexample is explicitly a $C^\infty$ object, so the conjecture's classical analytic form remains true. The gap between the two is the whole content of the result.
Known method families
construction (source-reported)
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
The source status is candidate and must not be represented as solved.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.