Erdős Problem a Daythe open tracker
The board / graph theory / #619

Erdős Problem #619

SOLVED LEANdatabase updated 2026-06-22

Resolved in some way other than a straight proof or disproof — usual for open-ended questions, or for multi-part problems whose parts went different ways. A solution has also been checked by machine, in Lean.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

For a graph \(G\), `minNewEdges r G` is the smallest number of edges that need to be added to \(G\) so that it has diameter at most \(r\), while preserving the property of being triangle-free. Erdős, Gyárfás and Ruszinkó denote this quantity by \(h_r(G)\) in [EGR98]. Adding edges is formalised as passing to a supergraph `H ≥ G` on the same vertex set, the number of added edges being the (finite) cardinality of the edge set of `H \ G`. We use the extended diameter `SimpleGraph.ediam` (valued in `ℕ∞`) so

**Erdős Problem 619** [EGR98, Er99]: For a triangle-free graph \(G\) let \(h_r(G)\) be the smallest number of edges that need to be added to \(G\) so that it has diameter \(r\) (while preserving the property of being triangle-free). Is it true that there exists a constant \(c>0\) such that if \(G\) is a connected graph on \(n\) vertices then \(h_4(G)<(1-c)n\)? The answer is **no**: for every \(\eta>0\) there exist connected triangle-free graphs on \(n\) vertices with \(h_4(G)\geq(1-\eta)n\), so no such constant \(c\) exists. The original proof was generated by Claude Fable 5; the Lean formalization was sketched by Fable and implemented by GPT 5.5 with Codex (see the linked `formal_proof`).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/619.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/619

Attempts

submit one →
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.

← #618the board#620 →