The inverse problem for the number of connected induced subgraphs

For a finite graph G, let c(G) be the number of nonempty vertex sets that induce a connected subgraph. We show that a positive integer k equals c(G) for some finite connected graph G if and only if k ∉ {2, 4, 5, 8, 9, 16}. Every attainable value k ≠ 25 is attained on ⌊log2 k⌋ + 1 vertices, the least possible number, and 25 needs six vertices. More precisely, for every m ≥ 6 each integer from 2m−1 to 2m − 1 is the value of c on a connected graph with exactly m vertices. The proofs of these results are short and use no computer; computer calculations serve only as independent checks, and for two auxiliary results: the values on six to eight vertices, and the result on all connected subgraphs described below. The value 16 falls into a gap above the path: a connected graph on n ≥ 4 vertices other than the path Pn has at least n − 3 more connected sets than Pn. The values k ≥ 17 are realized by a recursive construction from cones, disjoint unions and a family of graphs that we call near-cones, starting from seven small graphs; it produces a graph with c(G) = k in time polynomial in log k. The question arose from a problem of Ordoñez in continuum theory, through a reduction by Camargo, Ordoñez and Ramírez, who found the values up to 255 by a computer search. The proof is formalized in Lean 4. We also observe that a theorem of Czabarka, Székely and Wagner on subtrees reduces the corresponding problem for the number of all connected subgraphs to a finite computation, and we report its outcome. We did not find these results in the literature, but we make no claim of novelty or priority. Supplementary material. LaTeX source; a Lean 4 / Mathlib formalization (Lean 4.35.0, Mathlib commit 6015dbb, library ConnectedSets) of the results of Sections 2–6 and Lemma 7.2, using only Lean's standard axioms and checked with leanchecker and the external type checker nanoda; programs (Python and C) and their outputs. Status. Preprint; not yet peer reviewed, and no independent expert has yet verified the proofs. The main model used to solve the problem and prove the theorems was Claude Opus 5.5 (Anthropic); ChatGPT-Astra (OpenAI) was used with the author to read the manuscript and check the arguments. See AI_DISCLOSURE.md.