---

Claim. The answer to Problem 1036 is yes: for every $c>0$ there is $\delta>0$ such that, for all sufficiently large $n$, every graph $G$ on $n$ vertices with no complete and no empty induced subgraph on more than $c\log n$ vertices has at least $2^{\delta n}$ pairwise non-isomorphic induced subgraphs. The claimed result is Theorem 1.3 of S. Shelah, Erdős and Rényi conjecture, J. Combin. Theory Ser. A 82 (1998), no. 2, 179--185, DOI 10.1006/jcta.1997.2845 (Crossref record accessed; issued May 1998, whose nominal first day the paper link carries): for every $c_1>0$ there is $c_2>0$ such that, for $n$ large enough, a graph $G$ on $n$ vertices with neither a complete subgraph nor an edgeless subgraph on at least $c_1\log n$ vertices has $I(G)\ge2^{c_2n}$, where $I(G)$ is the number of induced subgraphs of $G$ up to isomorphism (Definition 1.2) and $\log$ is the base-two logarithm (Notation 1.1), a convention that changes $c_1$ by a constant factor only. The theorem's printed hypothesis reads "a graph with $n$ edges [sic]" in the arXiv version (card); the abstract, the conjecture as stated in the introduction and the proof concern a graph with $n$ vertices, and the claim recorded here is the vertex form. The site's "more than $c\log n$" and the theorem's "at least $c_1\log n$" differ by the choice of constant. The paper names the statement as a conjecture of Erdős and Rényi and records the earlier bounds: Alon and Hajnal's $I(G)\ge2^{n/2t^{20\log(2t)}}$ with $t$ the largest trivial subgraph, which for $t\le c\log n$ gives $\exp(n(\log n)^{-O(\log\log n)})$ (the introduction prints $t\ge c\log n$, a slip: the bound weakens as $t$ grows) (card), and the parallel theorem with the bipartite Ramsey function in place of the trivial-subgraph size, which the introduction credits to Erdős and Rényi; it is Theorem 2 of Erdős and Hajnal [ErHa89b] (card), as the site and Erdős's 1993 survey (card, Chapter V, problem 14) credit it: for $c>0$ and $k>2c\log2$, if neither $G$ nor its complement contains $K_{c\log n,c\log n}$, then $G$ has at least $2^{n/4k}$ pairwise non-isomorphic induced subgraphs for all large $n$; it has its own partial claim page, Erdős and Hajnal. Remark 1.4 blows up each vertex of a Ramsey graph into $m$ vertices, giving $I(G)\le2^{n\log_2(m+1)}$, and conjectures that this is the worst case.

Depends on. Nothing in this wiki.

Formalization. The file src/v4.29.1/ErdosProblems/Erdos1036.lean of Boris Alexeev's repository plby/lean-proofs (Lean v4.29.1 with Mathlib v4.29.1; 3,916 lines at the pinned commit of 2026-09-15, linked above), announced in the site's forum on 21 January 2026, declares itself a formalization of this result: its header names Shelah as the informal author and the automated prover Aristotle and Alexeev as formal authors, and its opening comment says that it formalizes the main theorem of the paper. Its final theorem erdos_1036 states that for every real $c>0$ there are $\varepsilon>0$ and $n_0$ such that every finite simple graph on $n\ge n_0$ vertices whose clique number and independence number are both at most $c\log_2 n$ (hom_num) has at least $2^{\varepsilon n}$ vertex subsets up to isomorphism of the induced graphs (I_num), the statement of the problem with the base of the logarithm rescaling $c$; a comment after #print axioms erdos_1036 reports the axioms propext, choice and Quot.sound, and the file contains no sorry, axiom, native_decide or unsafe. The repository's note ErdosProblems/Erdos1036.md (the record link) lists copies for five toolchains (Lean v4.24.0 to v4.33.0). Nothing was built, replayed or audited here, and the fidelity of its statement to the question was not independently reviewed by this project, so the page lists no formalized evidence.

Acceptance. Refereed publication in the Journal of Combinatorial Theory, Series A, cited with its venue above, the refereed evidence. The reviewed evidence is the site's documented acceptance: the site's curator, Thomas Bloom, labels the problem PROVED (LEAN) and credits Shelah [Sh98] with the proof in the commentary, revised after the forum comment of 13 September 2025 pointed to the paper, which Bloom acknowledged the same day (Bloom took no part in the paper); the proof-claim tab is empty, and the community database records "proved (Lean)". This page's date is the arXiv posting of 15 July 1997 (arXiv record accessed; the manuscript's own revision date is 14 August 1997). The paper is also posted as paper 627 in Shelah's archive (the second preprint link). Read depth here: the abstract, Notation 1.1, Definition 1.2, Theorem 1.3 and Remark 1.4 of the arXiv version; the proof was not read, and nothing is independently reviewed by this project.