Seymour's second-neighborhood conjecture
Seymour's second-neighborhood conjecture asserts that every nonempty finite oriented graph (no loops and no pair of oppositely directed edges) has a vertex with at least as many vertices at directed distance exactly two as at directed distance one. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof. This page summarizes the published claim and lists publicly available follow-up work.
Background
- According to the manuscript's introduction, the conjecture was recorded by Dean and Latka (1995). Its tournament case, Dean's conjecture, was proved by Fisher (1996) using a probability distribution obtained from Farkas' lemma, and Havet and Thomassé gave a combinatorial proof using local median orders; Fidler and Yuster extended the tournament theorem.
- The same introduction recalls that Kaneko and Locke (2001) proved the conjecture for minimum out-degree at most six, that a recent computer-assisted preprint treats minimum out-degree seven, and that Chen, Shen and Yuster proved a universal second-to-first neighborhood ratio of about 0.657298.
The original result
- Claim. Every nonempty finite oriented graph has a vertex with at least as many vertices at directed distance two as at directed distance one.
- Source. A proof of Seymour's second-neighborhood conjecture in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/173.md states that the formalized result proves the conjecture, with the second neighborhood taken as the vertices at directed distance exactly two (the initial vertex and the first neighbors excluded, sinks included). The Comparator statement is
SeymourSecondNeighborhood.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates the challenge SeymourSecondNeighborhood "full" and records a sandboxed Comparator pass. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list this challenge, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-15 (revised version listed) | A. Sadhukhan, S. Sen, Locating a Seymour vertex in oriented graphs having minimum outdegree at most 7 (arXiv:2606.30588) | Earlier partial result (cited by the manuscript); remark | Proves the conjecture for every oriented graph with minimum out-degree at most 7. The revised version states that OpenAI "has released a preprint presenting a proof of Seymour's Second Neighborhood Conjecture, with an accompanying Lean formalization", that "this can be considered as a work in parallel, since an earlier version of this paper was cited in the OpenAI preprint", and that, "barring the OpenAI's post", its result is the first improvement in more than two decades to the minimum-out-degree bound. | arXiv preprint (revised). |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.