Written on the Wall II, Graph Conjecture 217
- Result
- Proved
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Graph theory (automated conjecture)
- Posed by
- Written on the Wall II (automated conjecturing)
- Year posed
- —
- Years open
- —
- Solved
- 2026-07-30
- Model
- Claude Opus 5 (with Gemini 3.1 Pro, GPT-5.3 Codex Spark, Grok 4.5)
- Vendor
- —
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 5 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
Per the submitter's disclosure, the proof and submission preparation used Claude Opus 5, with the other models on bounded mechanical subtasks. A second, independent Lean proof of the same conjecture (ChatGPT 5.6 Sol and Codex) was submitted days earlier.
Verification
Kernel-checked Lean 4 proof; the axiom check includes native_decide (Lean.ofReduceBool / trustCompiler) for the exhaustive finite-graph certificates, which the submitter flags as the main trust assumption. Acceptance into the formal-conjectures repository is still pending, hence candidate status.