# Seymour’s second-neighborhood conjecture

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

- [A proof of Seymour’s second-neighborhood conjecture](../../preprints/A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/SeymourSecondNeighborhood.lean) |