Seymour’s second-neighborhood conjecture

Proves Seymour's second-neighborhood conjecture: every nonempty finite oriented graph has a vertex with at least as many vertices at directed distance exactly two as at directed distance one. Oriented graphs may be arbitrary apart from the exclusion of loops and oppositely directed edge pairs. (Lean)

Manuscript

A proof of Seymour’s second-neighborhood conjecture

September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026}

We prove that every nonempty finite oriented graph has a vertex with at least as many vertices at directed distance two as at directed distance one. This resolves Seymour's second neighborhood conjecture positively.

Result 173 · Combinatorics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.