The board / graph theory / #59
Erdős Problem #59
DISPROVED LEANdatabase updated 2026-08-24
The statement as posed is false. 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).
`numFree H n` is the number of labelled graphs on the vertex set `Fin n` which do not contain `H` as a subgraph.
Is it true that the number of graphs on \(n\) vertices which do not contain \(G\) is \[\leq 2^{(1+o(1))\mathrm{ex}(n;G)}?\] The answer is no, already for \(G=C_6\) (see `erdos_59.variants.morris_saxton`). Graphs are labelled, and \(G\) ranges over finite graphs containing a cycle, as in [MoSa16]; for some forests the answer is trivially no (for the path with two edges the free graphs include all matchings, about \(2^{\Theta(n\log n)}\) of them).
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/59.Prizenone
Topicsgraph theory, turan number
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/59
Attempts
submit one →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.