Seymour’s second-neighborhood conjecture

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A proof of Seymour’s second-neighborhood conjecture

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A proof of Seymour's second-neighborhood conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026/paper.pdf}{OAI:A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A proof of Seymour’s second-neighborhood conjecture

Scope

Seymour's second-neighborhood conjecture asserts that every nonempty finite oriented graph has a vertex with at least as many second out-neighbors as first out-neighbors. The formalized result proves this assertion, where the second neighborhood consists of vertices at directed distance exactly two. The initial vertex and first neighbors are excluded from that count, and sinks are included.

Comparator links

Result	Comparator statement
Seymour's second-neighborhood conjecture	SeymourSecondNeighborhood.lean

Scope note on GitHub →