Erdős problem 426
We say is a unique subgraph of if there is exactly one way to find as a subgraph (not necessarily induced) of . Is there a graph on vertices with many distinct unique subgraphs?
Sources
FormalConjectures/ErdosProblems/
426.lean
We say is a unique subgraph of if there is exactly one way to find as a subgraph (not necessarily induced) of . Is there a graph on vertices with many distinct unique subgraphs?
Bradač and Christoph [BrCh24] have proved the answer is no: if is the maximum number of unique subgraphs in a graph on vertices then
The below is read as: some constant works for arbitrarily large . The negation of the proposition on the right is then exactly , the form in which Bradač and Christoph [BrCh24] resolved the problem.
The linked file states the resolution in that negated form, as Tendsto fSeq atTop (nhds 0). It counts the isomorphism classes occurring as unique subgraphs, whereas uniqueSubgraphCount counts their representatives ; uniqueness forces exactly one representative per class, so the two counts agree.
False ↔ ∃ c, 0 < c ∧ ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, c * (2 ^ n.choose 2 / ↑n.factorial) ≤ ↑H.uniqueSubgraphCount