Problem detail · source-aware
VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
For every finite connected simple graph $G$, is the order of the largest induced tree at least $\mathrm{girth}(G) - 1 + \mathrm{ecc}(G, \mathrm{center}(G))$, where the last term is the eccentricity of the centre set? Answered affirmatively, with a Lean proof.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
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.
Provider: OpenAI · Prompt public: unknown · Independence: unknown
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.
Correctness: supported · statement fidelity: audited · peer review: none
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.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.