Aftermath bot: New page: OpenAI's proof claim with full Lean scope, MathVet, con-leche, and Sadhukhan-Sen's revised minimum-outdegree-7 preprint with its remark

2026-10-16T03:24:30Z

New page: OpenAI's proof claim with full Lean scope, MathVet, con-leche, and Sadhukhan-Sen's revised minimum-outdegree-7 preprint with its remark

New page

'''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 ([https://github.com/openai/math 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.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026 ''A proof of Seymour's second-neighborhood conjecture''] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/173.md 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 <code>SeymourSecondNeighborhood.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates the challenge <code>SeymourSecondNeighborhood</code> "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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, 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'' ([https://arxiv.org/abs/2606.30588 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.

[[Category:OpenAI results]]

Seymour's second-neighborhood conjecture - Revision history

Aftermath bot: New page: OpenAI's proof claim with full Lean scope, MathVet, con-leche, and Sadhukhan-Sen's revised minimum-outdegree-7 preprint with its remark