Seymour’s conjecture: two steps keep up?

The claim, in plain words

“An oriented graph is a finite directed graph with no loops, no multiple arcs, and no pair of opposite arcs.” For a vertex v, its out-neighbours are one arrow away, and its second neighbours are “the vertices at directed distance exactly two from v. Each vertex is counted once, regardless of the number of paths reaching it.” Seymour’s second-neighbourhood conjecture asks for a vertex with at least as many second neighbours as out-neighbours. In a directed triangle every vertex ties, one and one; in a ranked tournament only the sink works; and if two-way pairs were allowed, two vertices pointing at each other would each have one out-neighbour and no second neighbours. As the paper recounts, the conjecture was recorded by Dean and Latka (1995). For tournaments it was proved by Fisher (1996) and, with local median orders, by Havet and Thomassé; Kaneko and Locke handled minimum out-degree at most six; Chen, Shen and Yuster proved a ratio of approximately 0.657298, which Huang and Peng raised to approximately 0.715538 in a 2024 preprint.

Result 173 is a single OpenAI preprint, A proof of Seymour’s second-neighborhood conjecture (15 pages, dated September 23, 2026). Theorem 1.1: “Every nonempty finite oriented graph has a vertex v such that |N₁⁺(v)| ≤ |N₂⁺(v)|.” It “resolves the conjecture positively, without a connectivity or degree hypothesis.” The ratio is therefore 1, and the directed triangle shows it cannot be improved. The paper also derives the weighted forms through Seacrest’s equivalences (“the equivalences themselves are not new here”) and consequences for short cycles, including: “If δ⁺(D) ≥ n/3 and δ⁻(D) ≥ n/3, then D contains a directed 3-cycle.”

What it doesn’t claim

Only oriented graphs are covered: with two-way pairs the statement can fail, and infinite graphs are not discussed. The theorem promises some vertex, not every vertex, and says nothing about how many there are. The proof is by contradiction; once existence is known, checking every vertex finds one. In our own exhaustive search, no oriented graph with up to 7 vertices is a counterexample (2,142,288 isomorphism classes with 7 vertices), which of course proves nothing in general.

Where it stands

Posted as a preprint

OpenAI, 15 pages, dated September 23, 2026

Peer reviewed

Not yet

Checked in Lean

The main theorem, formalized by OpenAI; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statement matches Theorem 1.1 exactly: second neighbours are the vertices other than v, not already out-neighbours, reached by a two-step path, and sinks are allowed. By our count the proof takes 43 files and 4,861 lines excluding Mathlib (the development), with no unproved steps by our search; we have not rebuilt it. The weighted and short-cycle consequences are not formalized. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

1. Sets instead of single vertices. For a set S, F(S) is everything S points to. In a smallest counterexample (fewest vertices, then fewest arrows) there is no sink, every vertex has an arrow coming in, and, adapting an argument of Seacrest, every nonempty proper set S satisfies |F²(S) ∖ F(S)| < |F(S) ∖ S| (Lemma 2.2).
2. Inflating. Following Brantner, Brockman, Kay and Snively, each vertex is replaced by a ranked block (a transitive tournament) with more vertices than the whole graph has. In the new graph every nonempty proper set U satisfies |U| + |F²(U)| < 2|F(U)|: the sizes are strictly concave (Lemma 2.3, Proposition 2.1).
3. An extremal argument on pairs. On the grid of ordered pairs of vertices, one family moves its first coordinate along arrows and another its second; they are compatible when those images do not meet. Among compatible pairs of families containing the diagonal, take one maximizing their combined size M plus the number d of grid points left uncovered. The concavity makes the complements of the second images larger than M + 2d, but they may conflict (Proposition 4.1).
4. The pruning lemma. For any finite relation, the conflicts can be removed by deleting at most |H| members plus the number of conflict points left uncovered afterwards, where |H| ≤ d (Lemma 3.1). Its proof bounds a matching in an augmented bipartite graph using generic ranks of matrices with free-variable entries, and Kőnig’s theorem.
5. The contradiction. The pruned families score more than M + 2d − (d + d′) + d′ = M + d, contradicting the choice; so no counterexample exists.

The numbers in the video

• Our examples: the directed triangle (every vertex 1 and 1), the ranked tournament on 5 vertices (out-neighbours 4, 3, 2, 1, 0 and no second neighbours), and a two-way pair (1 and 0, failing).
• Our exhaustive search: every oriented graph up to 7 vertices (7, 42, 582, 21,480 and 2,142,288 isomorphism classes with 3 to 7 vertices), with no counterexample; also every labelled graph up to 5 vertices in Python.
• Our check of the concavity obstruction: all 16,292 labelled graphs with 3 to 5 vertices and every vertex entered have a set that breaks the inequality; for the triangle with doubled, unranked corners, single vertices satisfy it (1 + 2 < 2 · 2) but a pair does not (2 + 2 = 2 · 2).
• The Lean count: 43 files and 4,861 lines, our count of the import closure.

Read the source

• A proof of Seymour’s second-neighborhood conjecture (PDF), 15 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 173.

The paper

OpenAI groups related papers into one result; this one has a single paper.

• A proof of Seymour’s second-neighborhood conjecture

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.