Seymour's Second Neighbourhood Conjecture
OPG_seymour_second_neighborhood_outdegree
Source: Open Problem Garden: seymours_second_neighbourhood_conjecture
Status ai-proved high confidence
OpenAI's manuscript proves that every nonempty finite oriented graph has a vertex $v$ with $|N^+(v)| \le |N^{++}(v)|$, where $N^{++}(v)$ is the set of vertices at directed distance exactly two from $v$.
Cited literature (4)
-
Proves the conjecture holds asymptotically almost surely for all orientations of G(n,p) when lim sup p < 1/4, and for random orientations of pseudorandom graphs satisfying certain density conditions.
-
Proves the conjecture for almost all orientations of G(n,p) for any fixed p in [0, 1/2), and shows any minimum counterexample must be strongly connected with bounded minimum outdegree.
-
partial About the second neighborhood conjecture for tournaments missing two stars or disjoint paths (2024)
Proves Seymour's Second Neighbourhood Conjecture for tournaments missing two stars, and investigates the conjecture for tournaments missing disjoint paths of length 2.
-
partial Seymour's Second Neighbourhood Conjecture for Oriented Graphs of Order at Most Seven and Split-Twin Extensions (2026)
Computationally verifies the conjecture for all oriented graphs of order at most 7, and introduces a split-twin extension operation preserving Seymour vertices, generating infinite inductively-defined families satisfying the conjecture.
Reviewer notes. Literature status before this model-generated claim: partial. Seymour's Second Neighbourhood Conjecture remains open in general. Meaningful partial progress since 2007 includes confirmation for almost all orientations of random graphs $G(n,p)$ with fixed $p < 1/2$, for tournaments missing two stars, and via exhaustive computation for all oriented graphs of order at most seven. Structural reductions show that any minimum counterexample must be strongly connected with bounded minimum outdegree.
OpenAI manuscript collection ai-proved
- A proof of Seymour’s second-neighborhood conjecture — main result formalized in Lean by OpenAI
Family 173: Seymour’s second-neighborhood conjecture · Lean formalization scope
These manuscripts were produced by an unreleased OpenAI model and released on
2026-10-06 in github.com/openai/math.
They have not been peer reviewed. Lean formalizations are OpenAI's own and cover
only the scope stated on their scope page; this project has not run or reviewed them.
The status above records the claim; before it, the literature review rated this
entry partial. Its confidence rates
whether the manuscript's theorem settles this entry, not whether the manuscript
is correct.
Discussion
By the $ n $ th outdegree of $ v $ , we mean the number of vertices for which the minimal outward-directed path from $ v $ to them is of length $ n $ . Chen, Shen, and Yuster [CSY] proved that in any oriented graph there is a vertex whose second outdegree is at least $ \gamma $ times its outdegree, where $ \gamma=0.657298... $ is the unique real root of $ 2x^3+x^2 -1=0 $ . This conjecture implies a special case of the \Oprefnum[Caccetta-Häggkvist Conjecture]{46385}.
Bibliography
-
[ASY]Chen, G.; Shen, J.; Yuster, R. Second neighborhood via first neighborhood in digraphs, Annals of Combinatorics, 7 (2003), 15--20. -
[F]Fisher, David C. Squaring a tournament: a proof of Dean's conjecture. J. Graph Theory 23 (1996), no. 1, 43--48. -
[KL]Kaneko, Yoshihiro; Locke, Stephen C. The minimum degree approach for Paul Seymour's distance 2 conjecture. Proceedings of the Thirty-second Southeastern International Conference on Combinatorics, Graph Theory and Computing (Baton Rouge, LA, 2001). Congr. Numer. 148 (2001), 201--206.