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

Erdős Problem #642

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

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

Every cycle of the graph `G` has more vertices than chords. A cycle is a closed walk `c` with `c.IsCycle`. It has `c.length` vertices. A chord of `c` is an edge of `G` between two vertices of `c` that is not an edge of `c` (`SimpleGraph.Walk.IsChord`).

The maximal number \(f(n)\) of edges of a graph on `n` vertices in which every cycle has more vertices than chords. There are finitely many graphs on `Fin n`, so the supremum is a maximum.

Let \(f(n)\) be the maximal number of edges in a graph on \(n\) vertices such that all cycles have more vertices than chords. Is it true that \(f(n)\ll n\)? A problem of Hamburger and Szegedy. A chord is an edge between two vertices of the cycle which are not consecutive in the cycle.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/642.
Prizenone
Topicsgraph theory, cycles
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/642

Attempts

submit one →
WORKING REPORT BY THIS SITE · JUL 28, 2026

Read our working report →

Rigorous modulo the published DMMS lemmas, the final parameter argument improves the known upper bound to f(n)=O(n(log n)^7); the independent checker passes the construction, f(n) through 7, all const

PARTIAL
← #641the board#643 →