Seymour's second neighborhood conjecture
An oriented graph is a finite digraph with no loops, multiple arcs or pairs of opposite arcs. For a vertex let be its out-neighbours and the vertices at directed distance exactly two. Seymour conjectured that every nonempty oriented graph has a vertex with . The tournament case (Dean's conjecture) was proved by Fisher (1996); Kaneko and Locke proved it for minimum outdegree at most six, and later work treated tournaments missing a matching, star or clique, dense cases, and random orientations, with a best universal ratio of about 0.7155 (Huang-Peng). Does every nonempty finite oriented graph have such a vertex?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Directed graphs; oriented graphs and tournaments
- Posed by
- P. Seymour; recorded by N. Dean and B. J. Latka, Squaring the tournament - an open problem, Congressus Numerantium 109 (1995)
- Year posed
- 1995
- Years open
- 31y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 38 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: every nonempty finite oriented graph has a vertex with , with no connectivity, density or degree assumption. Via Seacrest's equivalences it also gives the vertex- and arc-weighted forms, and it yields short-cycle consequences, for example a directed triangle whenever minimum in- and outdegree are at least one third of the order. It does not address infinite digraphs or digraphs with 2-cycles, which the conjecture excludes.
What the AI did
Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems, published in the openai/math release (pinned commit adc7f12). The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is authored as OpenAI with no human author named. The main theorem has a Lean formalization in the release (Comparator challenge SeymourSecondNeighborhood).
Verification
No independent mathematician has checked this yet. Checked here: abstract, introduction and Theorem 1.1 of the TeX source, read against the conjecture as recorded by Dean and Latka. Lean-checked on the release's Comparator challenge SeymourSecondNeighborhood (declaration OAI.SeymourSecondNeighborhood.exists_goodVertex, listed in lean/formalization.yaml). Its statement was read here: for every nonempty finite type with a loopless asymmetric relation, some vertex has at most as many first out-neighbours as second neighbours, where second neighbours exclude the vertex itself and its out-neighbours and are reached by a two-step path. That is exactly the headline claim, with no connectivity or degree hypothesis. Not rebuilt here. The minimal-counterexample and pruning argument was not refereed.