ProofAtlas

Graph theory · formal theorem

Friendship Theorem

In a finite graph with at least two vertices, exactly one common neighbor for every distinct pair forces a universal hub; every other vertex has exactly one neighbor other than the hub.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
Friendship theorem statement mapFor a finite graph with at least two vertices, the unique-common-neighbor condition leads to a universal hub and the recorded local neighbor-uniqueness property.
Exact scope: For finite simple graphs with at least two vertices, exactly one common neighbor for every distinct pair forces a universal hub; every other vertex has exactly one neighbor other than the hub.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

The theorem at a glance

Friendship Theorem at a glance

Editorial theorem poster showing the unique-common-neighbor hypothesis, the forced universal hub and outer pair structure, the adjacency-matrix and spectral proof route, and the exact finite-simple-graph scope.
The Friendship Theorem turns one local common-neighbor rule into a universal hub and a precise pairing of every other vertex.

Accessible transcript

Every distinct pair has exactly one common neighbor ⇒ ∃ a universal hub c, and each v ≠ c has exactly one non-hub neighbor

Assuming no universal hub first forces regularity and the matrix identity A² = (k − 1)I + J. Its spectrum and trace relations produce an arithmetic contradiction, so a hub exists; the original common-neighbor rule then gives exactly one non-hub neighbor for every other vertex.

Read the complete poster transcript

GRAPH THEORY · FINITE SIMPLE GRAPHS

FRIENDSHIP THEOREM

ONE LOCAL RULE FORCES A GLOBAL HUB

EVERY DISTINCT PAIR

has exactly one common neighbor

u · v · w

AT LEAST TWO VERTICES

THEN ONE VERTEX TOUCHES EVERY OTHER

AND THE REST PAIR LOCALLY

Each non-hub vertex has exactly one non-hub neighbor.

a₁ · b₁ · a₂ · b₂ · ⋮ · c · ⋮ · aₘ · bₘ

HOW THE PROOF MOVES

1 · ASSUME NO HUB

All degrees become one common value k.

2 · COUNT TWO-STEP WALKS

A² = (k − 1)I + J

A² = [k−1 1 … 1; 1 k−1 … 1; ⋮ ⋮ ⋱ ⋮; 1 1 … k−1]

3 · READ THE SPECTRUM

Nonprincipal eigenvalues satisfy λ² = k − 1.

λ · √(k − 1) · −√(k − 1)

4 · FORCE THE CONTRADICTION

d² = k − 1 and d ∣ k ⇒ d = 1 ⇒ k = 2

EXACT SCOPE

Finite simple graphs with at least two vertices. The conclusion includes a universal hub and exactly one non-hub neighbor for every other vertex.

Theorem schematic

A local rule forces a universal hub

A gold universal hub connects to every outer vertex while the outer vertices form several distinct green-edged pairs, expressing both conclusions of the Friendship Theorem.
A unique common neighbor for every distinct pair forces one universal hub, with every other vertex having exactly one non-hub neighbor.

Every distinct pair has exactly one common neighbor ⇒ a universal hub exists and each non-hub vertex has exactly one non-hub neighbor

The unique-common-neighbor hypothesis forces a vertex adjacent to every other vertex. Once that hub is fixed, every remaining vertex has exactly one neighbor outside the hub, so the non-hub vertices split into disjoint adjacent pairs.

Proof architecture

Why one shared neighbor forces a universal hub

5 curated stages

The checked proof first assumes that no hub exists. It turns the graph into a strongly regular matrix problem, uses the Hermitian spectrum to force impossible degree arithmetic, and then returns to the graph to obtain the hub and exact pairing of every non-hub vertex.

These source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A balanced finite graph with no dominant vertex carries equal-degree structure, while two attached lenses trace distinct vertex pairs to one gold common-neighbor witness each.
    Under the temporary no-hub assumption, the common-neighbor rule forces one common degree and strongly regular parameters with both common-neighbor counts equal to one.
    01

    No hub forces strong regularity

    No hub ⇒ G is k-regular and IsSRGWith |V| k 1 1

    Assuming there is no universal vertex, the unique-common-neighbor rule forces every vertex to have the same degree. Adjacent and nonadjacent pairs each have exactly one common neighbor, giving the strongly regular parameters used in the rest of the proof.

    Lean lemmas for this step
    • degree_eq_of_no_hub
    • isRegularOfDegree_of_no_hub
    • isSRGWith_of_no_hub
    • card_commonNeighbors_eq_one_of_unique
  2. The same hub-free graph transforms into a square matrix whose diagonal cells collect repeated return-walk rosettes and whose off-diagonal cells each contain one gold two-step witness.
    Counting length-two walks turns strong regularity into the exact adjacency-matrix identity used by the checked spectral proof.
    02

    Two-step walks become a matrix identity

    A² = (k − 1)I + J

    Counting length-two walks gives k on each diagonal entry of A² and one on every off-diagonal entry. Separating the diagonal contribution yields the exact identity A² = (k − 1)I + J.

    Lean lemmas for this step
    • adjMatrix_sq_eq_diagonal_degree_sub_one_add_allOnes_of_no_hub
    • adjMatrix_sq_eq_diagonal_degree_sub_one_add_allOnes_of_no_hub_rclike
  3. An engraved matrix opens into cobalt Hermitian mode rails, with one isolated antique-gold degree mode and two balanced families of nontrivial modes feeding trace constraints.
    The matrix identity isolates the constant-vector degree mode and forces every nontrivial eigenvalue onto one of two symmetric square-root branches.
    03

    The spectrum has only three levels

    λ ≠ k ⇒ λ² = k − 1

    The constant vector has eigenvalue k. On its orthogonal complement, the matrix identity forces every eigenvalue λ to satisfy λ² = k − 1; trace and squared-trace identities then constrain the two possible multiplicities.

    Lean lemmas for this step
    • eigenvector_sum_eq_zero_of_eigenvalue_ne_degree_of_no_hub_rclike
    • eigenbasis_eigenvalue_sq_eq_degree_sub_one_of_ne_degree_of_no_hub_rclike
    • sum_hermitian_adjMatrix_eigenvalues_eq_zero
    • sum_sq_hermitian_adjMatrix_eigenvalues_eq_card_mul_degree_of_no_hub
  4. Cobalt spectral branches condense into a gold square-lattice witness and an equal-segment degree band, then meet a restrained vermilion broken joint opposite a four-spoke minimum-degree graph.
    The spectral trace relations produce a natural square-root witness dividing the degree, which collapses to degree two and contradicts the no-hub lower bound.
    04

    Spectral arithmetic closes the no-hub case

    ∃ d : ℕ, d² = k − 1 ∧ d ∣ k

    The spectral multiplicities yield a natural number d with d² = k − 1 and d dividing k. These arithmetic conditions force k = 2, contradicting the lower degree bound established under the no-hub assumption.

    Lean lemmas for this step
    • exists_nat_sq_sub_one_and_dvd_of_sum_roots
    • spectral_degree_condition_of_no_hub
    • not_exists_sq_degree_sub_one_dvd_degree_of_no_hub
    • four_le_degree_of_no_hub
  5. A fading hub-free graph resolves into one luminous gold hub with twelve green spokes and six isolated two-vertex outer pairs, with clear gaps between every pair-edge.
    Once the no-hub case is eliminated, one vertex touches every other vertex and each non-hub vertex has exactly one non-hub neighbor.
    05

    The hub and exact outer pairing

    ∃ c, IsHub G c ∧ NonHubHasExactlyOneNonHubNeighbor G c

    Eliminating the no-hub case produces a universal vertex c. The common-neighbor condition then forces every vertex other than c to have exactly one neighbor outside c, so the non-hub vertices are partitioned into disjoint adjacent pairs.

    Lean lemmas for this step
    • exists_hub_of_unique
    • nonHubHasExactlyOneNonHubNeighbor_of_isHub
    • friendshipTheorem_of_exists_hub
    • friendshipTheorem

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def FriendshipTheoremStatement : Prop :=
  ∀ (V : Type) [Fintype V] [DecidableEq V] [Nontrivial V]
    (G : SimpleGraph V),
    UniqueCommonNeighborProperty G →
      ∃ c : V, IsHub G c ∧ NonHubHasExactlyOneNonHubNeighbor G c
Definitions used in this proposition

UniqueCommonNeighborProperty

def UniqueCommonNeighborProperty (G : SimpleGraph V) : Prop :=
  ∀ v w : V, v ≠ w → ∃! u : V, IsCommonNeighbor G v w u

IsHub

def IsHub (G : SimpleGraph V) (c : V) : Prop :=
  ∀ v : V, v ≠ c → G.Adj c v

NonHubHasExactlyOneNonHubNeighbor

def NonHubHasExactlyOneNonHubNeighbor (G : SimpleGraph V) (c : V) : Prop :=
  ∀ v : V, v ≠ c → ∃! w : V, w ≠ c ∧ G.Adj v w
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem friendshipTheorem :
    FriendshipTheoremStatement
Open main Lean file

Result boundary

What this page does—and does not—establish

For finite simple graphs with at least two vertices, exactly one common neighbor for every distinct pair forces a universal hub; every other vertex has exactly one neighbor other than the hub.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Continue the mathematics

Start from the complete checked source

The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal-result publication and review details

Independent publication review

The formal theorem's publication gates are accepted

Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.

01

Formal evidence

Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image in a new tab