The board / graph theory / #65
Erdős Problem #65
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).
Let \(G\) be a graph with \(n\) vertices and \(kn\) edges, and \(a_1<a_2<\cdots\) be the lengths of cycles in \(G\). Assume \(n>0\). Is it true that \[\sum\frac{1}{a_i}\gg \log k?\] Gyárfás, Komlós, and Szemerédi [GKS84] have proved that this sum is \(\gg \log k\), so that only the second question remains. The bound is stated for all sufficiently large \(k\): [GKS84, Theorem 4'] proves it for \(k \geq b\), where \(b\) is a constant. The case of \(k\) slightly larger than \(1\) is a separate problem, studied in [GPSV85].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/65.Prizenone
Topicsgraph theory, cycles
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/65
Attempts
submit one →Read our working report →
Exhaustively verified the exact complete-bipartite minimum and uniqueness for every \(4\le n\le10\) and \(2\le d\le\lfloor n/2\rfloor\); the unresolved step is a uniform fixed-small-\(d\), all-\(n\) s
PARTIAL