Source and verification
This article explains family 173 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.
🏷️ First and second out-neighborhoods
An oriented graph is a finite directed graph with no loops and no pair of opposite arcs. It need not have an arc between every pair of vertices. For a vertex , let be its out-neighbors, and let consist of vertices at directed distance exactly two from .
Thus excludes both and the first out-neighbors. A vertex reached by several two-step paths is counted only once.
Manuscript claim
Every nonempty finite oriented graph has a vertex with . No connectivity or degree assumption is required. (OpenAI, 2026)
This is Seymour’s second-neighborhood conjecture. A sink satisfies it immediately, with both sides zero. The nontrivial case has positive outdegree everywhere. A directed triangle also gives equality at each vertex: one first neighbor and one distinct second neighbor.
Counting directed paths instead of distinct second neighbors would miss the issue. Many paths can merge at the same endpoint, and some endpoints may already be first neighbors.
🏷️ A set-image formulation
For a vertex set , define its forward image
This operation does not subtract . Because an oriented graph has no two-step return to its starting vertex,
Suppose a counterexample exists, and choose one first with minimum vertex count and then with minimum arc count. The source’s edge-deletion reduction gives, for every nonempty proper ,
This is stronger than simply applying the supposed failure at individual vertices. It controls arbitrary subsets and uses both minimality choices.
The manuscript next replaces each vertex by a sufficiently large transitive tournament, an orientation of a complete graph induced by a linear order. The resulting graph has positive indegree at every vertex and satisfies
for every nonempty proper . The rest of the argument proves that no finite graph arising in this way can have this strict concavity property for all subsets.
🏷️ Compatible families of ordered pairs
Work in . Advancing the first coordinate of a pair means following an arc of in that coordinate and keeping the second fixed; advancing the second coordinate is defined similarly.
Take two families of pairs, a left family and a right family. Call them compatible if the first-coordinate image of the left family is disjoint from the second-coordinate image of the right family. Require both families to contain the diagonal pairs . The absence of opposite arcs makes the diagonal families compatible, so admissible choices exist.
A point outside both coordinate images is uncovered. Write for the sum of the sizes of the two families and for the number of uncovered points. Among all compatible choices containing the diagonal, maximize
The diagonal and positive indegree conditions ensure that the columns of the left family and the rows of the right family are nonempty proper subsets. The strict concavity inequality therefore applies to each. Taking complements of second iterated images produces prospective new families whose combined size exceeds .
These larger families need not be compatible. Repairing that failure without spending the entire gain is the central problem.
🏷️ A pruning cost paid by uncovered points
The source proves a pruning lemma for arbitrary finite binary relations. It deletes conflicting members while preserving specified conflict-free members, which here include the diagonal. Let be the number of points uncovered by the retained families after pruning.
In the application, the deletion cost is at most . Thus the new objective is strictly greater than
contradicting maximality. The cancellation shows why the lemma must use the number of points uncovered after deletion. A bound expressed only in terms of the old uncovered set need not support this argument.
The pruning proof represents conflicts by an augmented bipartite graph and bounds a matching in it. Advancing the two coordinates in opposite orders yields two factorizations of the same matrix through different index sets. A simultaneous maximum-rank choice makes the corresponding kernels control the matching size. This is the new finite-dimensional ingredient; the extremal calculation alone would be incomplete without it.
🏷️ Scope of the conclusion
The paper also derives weighted versions through established equivalences. Two different quantifier orders arise: for every nonnegative vertex weighting there exists a suitable vertex, and there exists a probability weighting for which every vertex is suitable. They should not be conflated.
The unweighted theorem already follows from the chain described above: a minimal counterexample yields strict subset concavity; that concavity enlarges a compatible pair of families; the pruning estimate converts the enlargement into a strict improvement of a finite extremal objective. Each reduction is necessary to make the final contradiction apply to general oriented graphs rather than only tournaments.
🏷️ Key steps and proof outlines
The pruning problem needs an augmented graph
For left pairs and right pairs , a conflict means and . Let contain the output corners of conflicts and their opposite corners . The pruning lemma seeks conflict-free subfamilies with deletion cost at most plus the number of points of left uncovered afterward. (OpenAI, 2026)
Build a bipartite graph with original left and right members and two separate copies of . Join conflicting original members, and join each original member to the opposite copy of every point it covers. One conflict contributes the path below; distinct conflicts may share vertices.
flowchart TB ZL["output corner in Z left"] --- C["right member (i,s)"] C --- R["left member (p,j)"] R --- ZR["output corner in Z right"]
Suppose this graph has a vertex cover of size at most . Delete its original members. If output corners become uncovered, each of the remaining corners has a surviving covering member, so the opposite copy of that corner must belong to . Hence at most
original members were deleted. Initially conflict-free members are isolated even in the augmented graph and can be retained. Thus the exact desired deletion bound reduces to bounding a maximum matching.
Two coordinate orders give the same matrix
Choose a maximum matching with as few original-original edges as possible. Let count those edges, and let count its original-to-copy edges on the two sides. The latter matchings are individually maximum in their respective subgraphs: an augmenting path would either enlarge the whole matching or replace an original-original edge and decrease .
Using coefficients and on allowed arrows, define linear maps along the two routes
The first route changes the first coordinate forward and then the second backward; the second reverses that order. For each conflicting input-output pair, both matrix products have the single contribution . Thus exactly.
The source chooses one coefficient assignment with , , and the needed local support ranks maximal simultaneously. For each requirement choose a minor that is a nonzero polynomial in the coefficients. Their finite product is still nonzero, even when variables are shared, so one real assignment makes all requirements hold.
A maximum-rank support forces complementary kernel zeros
Kernel lemma
If has maximum rank among matrices with a prescribed support, then at every allowed entry whenever and .
If , perturb only that entry: . Then , so belongs to the new image. Every old image vector also belongs to it because . Yet is outside the old image, since the left-kernel vector has . Rank would increase, a contradiction.
Apply this lemma to the source’s coordinate blocks. It implies that a vector in must vanish at each of the original left endpoints, by pairing it with a suitable vector in equal to one at the matched right endpoint. Meanwhile the basis columns of allow each original left endpoint to be lifted to a vector with its own endpoint coordinate one and the others zero. The vectors are independent: a linear relation would put their corresponding linear combination in , forcing every coefficient to vanish.
Since , these vectors lie in . Rank-nullity now gives
The matching has size . The alternating-path proof of the bipartite matching-cover theorem supplies the required cover and hence the pruning.
The extremal objective absorbs the final uncovered set
In the graph reduction, take compatible pair families containing the diagonal and maximizing , where is their total size and counts uncovered points. Positive indegrees ensure that each relevant row and column is nonempty and proper, so strict subset concavity applies. Complements of the second coordinate images then have total size greater than .
The diagonal remains conflict-free in these larger families, and their opposite conflict corners lie in the old uncovered set, so . Pruning costs at most , where is the new uncovered count. The new objective therefore exceeds , contradicting maximality. This is why the pruning lemma must charge the uncovered points after deletion: their cost cancels exactly in the extremal objective.
See Also
- Crossing-number formulas uses matrix rank and subspace dimensions for another global graph inequality.
- Strong thin trees also depends on preserving structural constraints during deletion of graph data.
🏷️ Manuscripts and verification scope
- A proof of Seymour’s second-neighborhood conjecture — pinned manuscript and companion source.
The family scope page describes selected formalization coverage. The selected statement is the unweighted second-neighborhood theorem, including sinks and excluding first neighbors from the second count. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.
OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.