The board / graph theory / #180
Erdős Problem #180
DISPROVED LEANdatabase updated 2026-08-02
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).
A finite graph, bundled with its vertex count, so that a family may mix orders.
A host graph is `family`-free when it contains no member of `family` as a subgraph.
\(\mathrm{ex}(n;\mathcal{F})\), the greatest number of edges of a graph on `n` vertices containing no member of `family`.
If \(\mathcal{F}\) is a finite set of finite graphs then \(\mathrm{ex}(n;\mathcal{F})\) is the maximum number of edges a graph on \(n\) vertices can have without containing any subgraphs from \(\mathcal{F}\). Note that it is trivial that \(\mathrm{ex}(n;\mathcal{F})\leq \mathrm{ex}(n;G)\) for every \(G\in\mathcal{F}\). Is it true that, for every \(\mathcal{F}\), there exists \(G\in\mathcal{F}\) such that \[\mathrm{ex}(n;G)\ll_{\mathcal{F}}\mathrm{ex}(n;\mathcal{F})?\] This is the Erdős–Simonovits compactness conjecture. The answer is no: OpenAI [OpenAI26] give a family of connected bipartite graphs, none of them acyclic, for which no single member controls the family extremal number. See `erdos_180.variants.counterexample`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/180.Prizenone
Topicsgraph theory, turan number
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/180
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.