launch-corpus · graph-theory · open-problem · graph-reconstruction · graph-isomorphism
The deck of a finite graph G is the multiset of isomorphism classes of the vertex-deleted subgraphs G − v over all vertices v. If two finite simple graphs on at least three vertices have the same deck, must they be isomorphic?
Why it matters
Open Problem Garden rates the problem "Outstanding". Wikipedia records that it has been verified by McKay for all graphs on at most 13 vertices, that Bollobás showed almost all graphs are reconstructible, and that it reduces to the case of 2-connected graphs.
Mathematical status
Open: Open Problem Garden lists it as an open conjecture of Kelly and Ulam, and Wikipedia reports only verification up to 13 vertices and special families (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Open Problem Garden entry: deck definition, statement for graphs on ≥ 3 vertices, attribution to Kelly (1957) and Ulam (1960) (checked 2026-09-11): https://www.openproblemgarden.org/op/reconstruction_conjecture
Formal definitions of deck and hypomorphism, verification results and partial results (checked 2026-09-11): https://en.wikipedia.org/wiki/Reconstruction_conjecture
Local target: Corpus.Reconstruction.conjecture
Source SHA-256: d2c07d9ebf6c9b91dbc1eddc1deab88613f333ee1b5929f91ddf6da3a2df37ac
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For finite simple graphs G on V and H on W (Mathlib SimpleGraph, Fintype vertices) with at least three vertices, if there is a bijection σ : V ≃ W with G.induce {v}ᶜ isomorphic (≃g) to H.induce {σ v}ᶜ for every v, then G ≃g H is nonempty; the bijection encodes equality of the mul
No public records on this page.
No public records on this page.