Second Neighborhood Problem

Second Neighborhood Problem

OpenAI's claim

Seymour second neighborhoods: The paper claims that every finite nonempty oriented graph has a vertex whose second out-neighborhood is at least as large as its first. The second neighborhood excludes vertices already reachable in one step.

Mathematical statement of the claimed result

Mathematical claim 1.

For a nonempty finite oriented graph $D$, with no loops or oppositely directed pair of edges, let $N_1^+(v)$ be the out-neighbors and $N_2^+(v)$ the vertices at directed distance exactly two. The claimed theorem gives \[\exists v\in V(D):\quad|N_1^+(v)|\le|N_2^+(v)|.\] For triangle-free $D$ a corollary yields a vertex with $d^+(v)\le|Z(v)|$ and $n-1\ge2d^+(v)+d^-(v)$, where $Z(v)$ consists of non-neighbors excluding $v$. Hence $\delta^+\ge n/3$ and $\delta^-\ge n/3$ force a directed triangle; a digraph regular in both directions with degree $r$ and girth four has $n\ge3r+1$. These consequences require the specified in-degree conditions and do not give the full out-degree-only Caccetta--Häggkvist assertion.

Outline of the argument

Seymour second neighborhoods: A smallest counterexample is pruned to yield strict neighborhood inequalities for all proper vertex sets. Replacing vertices by transitive tournaments strengthens these to a discrete concavity inequality. Extremal families of ordered pairs and an augmented bipartite matching are then controlled by two factorizations of one matrix, contradicting that inequality.

Formal verification

Family 173 describes Lean coverage for the exact second-out-neighborhood inequality for a suitable vertex of every finite nonempty oriented graph.

Seymour second neighborhoods: The manuscript links SeymourSecondNeighborhood.lean (declaration OAI.SeymourSecondNeighborhood.exists_goodVertex).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, A proof of Seymour's second-neighborhood conjecture, 2026-09-23; citation key OAI:A-proof-of-Seymours-second-neighborhood-conjecture-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: cor:directed-cycle-consequences.
• Family 173: Lean scope.
• Comparator SeymourSecondNeighborhood.json.
• Comparator SeymourSecondNeighborhood.lean.
• OpenAI catalogue entry.

The Second Out-Neighbourhood Conjecture

Definitions and mathematical statement

Shared notation.

Unless a section says otherwise, ${\mathbb{N}}=\{1,2,\ldots\}$, ${\mathbb{Z}}$ is the ring of integers, ${\mathbb{Q}},{\mathbb{R}},{\mathbb{C}}$ are the rational, real, and complex fields, $[N]=\{1,\ldots,\lfloor N\rfloor\}$, and $\log$ is the natural logarithm. For real functions of a parameter tending to infinity, $f\ll g$ and $f=O(g)$ mean $|f|\leq Cg$ eventually for some fixed $C$; $f\gg g$ reverses this comparison; $f=o(g)$ means $f/g\to0$; $f\sim g$ means $f/g\to1$; and $f\asymp g$ means both order bounds. A subscript on $O$ or $\ll$ specifies allowed constant dependence. The expression $n^{o(1)}$ in an upper bound means growth smaller than $n^\epsilon$ for each fixed $\epsilon>0$. Local definitions govern any exception, finite-field convention, or use of the same symbol for another object. An asymptotic claim is not automatically an effective algorithm.

An oriented graph has no loops and never has both $u\to v$ and $v\to u$. Let $N^+(v)$ consist of vertices reached by one arc and $N^{++}(v)$ of vertices whose shortest directed distance from $v$ is exactly two. The conjecture asks for a vertex with $|N^{++}(v)|\geq|N^+(v)|$ in every finite oriented graph. [S1] [S2]

Statement recorded in the supplied source.

Does every oriented graph have a vertex with at least as many vertices at distance 2 as at distance 1? [S1]

Short English statement

Must some vertex in every finite oriented graph reach at least as many vertices for the first time in two steps as it reaches in one step?

Research attempt

Status and convention.

This is an unresolved attempt at Seymour's conjecture. In particular, $N^{++}(v)$ excludes both $v$ and $N^+(v)$, even when some out-neighbor also has a two-step walk from $v$. The calculation below proves the target when the minimum out-degree is at most two and for orientations of triangle-free graphs, and gives a general half-size bound. These are elementary subcases, not improvements on the literature. The June 2026 preprint of Sadhukhan, Sandeep and Sen reports the case of minimum out-degree seven, with part of its proof verified by CP-SAT; its abstract also records the previous threshold six. Those external results are distinguished from the local proofs and enumerations here. https://arxiv.org/abs/2606.30588

A local counting inequality.

Choose a minimum-out-degree vertex $v$, set $d=d^+(v)$, $A=N^+(v)$ and $B=N^{++}(v)$, and write $b=|B|$. If $d=0$, the target holds at $v$. Suppose $d>0$. Every out-neighbor of a vertex $u\in A$ lies in $A\cup B$. It cannot be $v$, because the digraph has no pair of opposite arcs; if it is outside $A\cup\{v\}$ it lies at distance exactly two from $v$. Summing the out-degrees of vertices of $A$ gives \[ d^2\leq\sum_{u\in A}d^+(u)=e(A)+e(A,B) \leq\binom d2+db. \] Here $e(A)$ counts arcs internal to $A$ once, and the last inequality uses at most one arc per unordered pair inside $A$, and at most one arc from each vertex of $A$ to each vertex of $B$. Thus \[ |N^{++}(v)|\geq\left\lceil\frac{d+1}{2}\right\rceil. \] For $d=1,2$ this lower bound is $d$, proving the conjecture in those cases. More precisely, retaining the actual internal arc count yields $b\geq\lceil d-e(A)/d\rceil$. That refinement identifies the loss in the argument: out-degree can be absorbed by arcs inside the first neighborhood instead of producing new second neighbors.

Triangle-free underlying graphs.

If the underlying undirected graph is triangle-free, there are no arcs between vertices of $A$: any such edge, together with their edges to $v$, would form a triangle. Fix $u\in A$. All $d^+(u)$ out-neighbors then lie in $B$, so $b\geq d^+(u)\geq d$. This proves the target directly, without regularity or a bound on the number of vertices. It also shows why bounding internal structure in $A$ can improve the half-size bound. For an arbitrary oriented graph, however, $A$ may itself be a tournament; no triangle-free conclusion is available.

Reduction to a terminal strongly connected component.

Contract the strongly connected components to obtain a finite acyclic digraph. It has a terminal component $C$ with no arc leaving it. For every $v\in C$, its first and second out-neighborhoods computed in the whole digraph are exactly those computed in the induced graph on $C$. Thus a good vertex of $C$ is good in the whole graph. A singleton terminal component is a sink and already settles the question. Consequently it would suffice to prove the conjecture for strongly connected oriented graphs. This is a valid reduction, but it does not bound their orders or degrees and is not itself a proof of the target.

Why a degree threshold alone cannot finish the problem.

Given an oriented graph $G$ and an integer $t\geq1$, replace every vertex by an independent set of $t$ clones and replace each arc $u\to v$ by all $t^2$ arcs from the $u$-clones to the $v$-clones. No loops or opposite arcs appear. For a clone $x$ of $v$, its first neighborhood is the union of the clone classes of $N^+(v)$, and its second neighborhood is exactly the union of those of $N^{++}(v)$. In particular, \[ d^+(x)=t d^+(v),\qquad |N^{++}(x)|=t|N^{++}(v)|. \] There is no new two-step route into $v$'s own clone class: such a route would require opposite arcs in $G$. A hypothetical counterexample would therefore produce counterexamples with arbitrarily large minimum out-degree by increasing $t$. This conditional construction is not a counterexample; it explains why a fixed verified degree threshold does not remove the general obstruction.

Exact finite check.

The companion script enumerates all labeled oriented graphs on one through five vertices. For each unordered pair it chooses no arc or one of the two directions, giving $3^{\binom n2}$ graphs at order $n$. It forms $N^{++}(v)$ as the union of the out-neighborhoods of $N^+(v)$, then removes $v$ and $N^+(v)$. It checks both the existence of a good vertex and the displayed bound at every minimum-out-degree vertex. This is a complete finite enumeration at those orders, including disconnected graphs, rather than a random search. It offers no uniform inference for larger orders.

Remaining obstruction.

The local estimate falls short when many arcs lie inside $A$ or when arcs from different vertices of $A$ repeatedly hit the same vertices of $B$. Summing out-degrees counts those repetitions, whereas the conjecture counts distinct endpoints. A full proof would need a rule for selecting a different vertex or exploiting these overlaps that forces $b\geq d$ somewhere. No such rule is established here, and the conjecture remains unresolved by this attempt.

Sources

• S1 ULAM.AI, UnsolvedMath, supplied problems.json, record 1441 (GRAPH-054), statement and background. The embedded literature-review date is 2026-08-17; that is the archive’s review date, not a fresh certification. Dataset landing page: https://huggingface.co/datasets/ulamai/UnsolvedMath.

• S2 D. C. Fisher, Squaring a tournament: a proof of Dean's conjecture, Journal of Graph Theory 23 $1996$, 43–48. https://doi.org/10.1002/(SICI)1097-0118(199609)23:1%3C43::AID-JGT4%3E3.0.CO;2-K. Bibliographic information from the supplied record.

• S3 Arpan Sadhukhan, R. B. Sandeep, and Sagnik Sen, A proof of Seymour's second neighborhood conjecture for oriented graphs with minimum out-degree equal to 7, arXiv:2606.30588 $2026$. https://arxiv.org/abs/2606.30588. Bibliographic information from the supplied record.

• S4 Yandong Bai, Binlong Li, and Boram Park, Towards a strengthening of the second neighborhood conjecture, arXiv:2607.18047 $2026$. https://arxiv.org/abs/2607.18047. Bibliographic information from the supplied record.