The $C^\infty$ Carathéodory Conjecture on Umbilic Points

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.

Exact FrontierDelta

Prior state unknown→disproved

Scope and record

Occurred: Aug 19, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-checked. Publication: announcement. AI contribution: ai-assisted. Imported under CC BY 4.0.

Canonical aliases: The $C^\infty$ Carathéodory Conjecture on Umbilic Points · Carathéodory conjecture (smooth)

Confidence: Not scored

Registry verification: lean checked · announcement · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

Levent Alpöge
human · human collaborator

John-Paul Smith
human · human collaborator

Claude
model · ai model contributor · Anthropic

Codex
model · ai model contributor · OpenAI

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: The $C^\infty$ Carathéodory Conjecture on Umbilic Points

specialist registry · passed

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.

Source ↗

The $C^\infty$ Carathéodory Conjecture on Umbilic Points

witness · pending

Primary source named by the VibeMathed record. Presence in this import is not an independent mathematical verification.

Source ↗

Lean proof, sorry-free at the pinned commit

lean artifact · pending

lean-proof link supplied by the VibeMathed registry.

Source ↗

The informal proof accompanying the formalization

paper · pending

paper link supplied by the VibeMathed registry.