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

Erdős Problem #1036

PROVED LEANdatabase updated 2026-01-20

The statement as posed is true, and a proof exists. 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).

`G` contains at least `k` many induced subgraphs which are not pairwise isomorphic, that is, there is a family of at least `k` many sets of vertices whose induced subgraphs are pairwise non-isomorphic.

Neither `G` nor its complement contains a balanced complete bipartite graph \(K_{k,k}\) on more than `m` vertices as a (not necessarily induced) subgraph. That is, there are no two disjoint sets of `k` vertices with \(2k > m\) such that every pair of vertices from different sets is adjacent in `G`, or every such pair is non-adjacent in `G`.

Let \(G\) be a graph on \(n\) vertices which does not contain a trivial (empty or complete) graph on more than \(c\log n\) vertices. Must \(G\) contain at least \(2^{\Omega_c(n)}\) many induced subgraphs which are not pairwise isomorphic? This is true, and was proved by Shelah [Sh98].
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/1036.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1036

Attempts

submit one →
NOBODY HAS SENT US AN ATTEMPT YET

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.

← #1035the board#1037 →