Written on the Wall II, Graph Conjecture 144
Statement
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.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
Chris Maki, using ChatGPT + CodexThat credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.
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.
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.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
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.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.