Codex 校核（2026-10-09） OpenAI 当前 cdc-lean 仓库已提供有限无自环、无桥多重图的无条件 cycle double cover 定理形式化，README 声称由 Lean 内核检查，并给出固定 Lean/Mathlib 版本与公理审计方法。因此“没有 Lean/Coq、仅人工审查”是7月初历史状态，不能作为当前结论。本次只读仓库文档，没有安装 Lean 或本地复跑。数学家 Jim Geelen 的解释发表于7月16日，Sang-il Oum 的解释当前 v3 为8月1日。单个定理和论文不能证明所有数学任务上的通用可靠性；“Wikipedia 首个”“能力阶跃”保留为当时报告与评估，未做全历史优先权审计。

GPT-5.6 Sol Ultra Produces Proof of the Cycle Double Cover Conjecture

Source: https://news.ycombinator.com/item?id=48863490 (205pts, 183comments) Original: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf

Core Facts

• OpenAI’s GPT-5.6 Sol Ultra produced a proof of the Cycle Double Cover Conjecture — a known unsolved problem in graph theory listed on Wikipedia’s “List of unsolved problems in mathematics.”
• The proof and writeup were entirely produced by the AI (via Codex with GPT 5.6 Sol).
• OpenAI released the prompt alongside the proof.
• Community debate centers on whether the proof is actually correct (no formal verification tool like Lean was used).

Significance

This is a landmark event in AI capability — it’s the first known instance of an LLM solving a problem notable enough to appear on Wikipedia’s list of unsolved mathematical problems. Previous AI mathematical breakthroughs (like AlphaTensor, AlphaGeometry) used specialized architectures, not general-purpose LLMs.

Community Reaction

• Skepticism: “Assume for purposes of this task that a complete affirmative proof exists” — some question the prompt’s framing
• Verification concerns: No proof assistant (Lean/Coq) was used — “But is the proof accepted to be correct?”
• Historic framing: “Is this the first LLM-solved problem famous enough to have been on Wikipedia’s list of unsolved problems?”

Impact Assessment

• Signal strength: 🔴 High — this represents a step-change in AI mathematical reasoning
• For agents: Demonstrates that frontier models can now produce novel mathematical proofs, opening up agent capabilities in research domains
• Caveat: Lack of formal verification means the proof may contain errors — community peer review needed