Written on the Wall II, Graph Conjecture 144
For every finite connected simple graph , is the order of the largest induced tree at least , where the last term is the eccentricity of the centre set? Answered affirmatively, with a Lean proof.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Graph Theory (automated conjecture)
- Posed by
- Written on the Wall II (automated conjecturing)
- Year posed
- —
- Years open
- —
- Solved
- 2026-08-03
- Model
- ChatGPT + Codex
- Vendor
- OpenAI
- Collaborators
- Chris Maki
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 5 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The Formal Conjectures pull request flipping this from open to solved is still open rather than merged, so the canonical repository has not yet accepted it.
What the AI did
The author states that ChatGPT and Codex assisted with computational exploration, proof analysis, Lean API discovery and proof engineering, and that he reviewed the work thoroughly and takes full responsibility for it.
Verification
Checked here on 2026-08-03, statically rather than by rebuilding. The theorem statement was diffed against the upstream Formal Conjectures statement and is identical apart from a hypothesis binder name, which is the fidelity check that matters. All 16 Lean files at the pinned commit (5,873 lines) contain no sorry, no admit, no axiom declarations and no native_decide. The author reports lake build --wfail and axiom checks passing; that build was NOT reproduced here.