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

Erdős Problem #627

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).

`maxChromaticCliqueRatio n` is \(f(n)\), the maximum of \(\chi(G)/\omega(G)\) over all graphs \(G\) on \(n\) vertices. A graph on `Fin n` is finite, so its chromatic number (an element of `ℕ∞`) is finite and `ENat.toNat` returns it. The maximum is taken over the finitely many graphs on `Fin n`, so the supremum is attained. For \(n = 0\) the only graph is empty, with \(\chi = \omega = 0\), and the convention \(0 / 0 = 0\) gives \(f(0) = 0\); this does not affect any asymptotic statement below.

Let \(\omega(G)\) denote the clique number of \(G\) and \(\chi(G)\) the chromatic number. If \(f(n)\) is the maximum value of \(\chi(G)/\omega(G)\), as \(G\) ranges over all graphs on \(n\) vertices, then does \[\lim_{n\to\infty}\frac{f(n)}{n/(\log_2n)^2}\] exist? Since \(f(n) \asymp n/(\log_2 n)^2\) (see `Erdos627.erdos_627.variants.theta`), the limit, if it exists, is a finite real number.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 8 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/627.
Prizenone
Topicsgraph theory, chromatic number
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/627

Attempts

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

Read our working report →

Exact, reproducibly checked values are \(f(n)=1\) for \(1\le n\le4\), \(f(n)=3/2\) for \(5\le n\le10\), and \(f(n)=2\) for \(11\le n\le16\); the asymptotic limit remains open.

PARTIAL
← #626the board#628 →