A proof of Seymour's second neighborhood conjecture for oriented graphs with minimum out-degree equal to 7

We prove Seymour's second neighborhood conjecture on oriented graphs whose minimum out-degree is equal to $7$.

This gives, to our knowledge, the first improvement of the minimum out-degree threshold in two decades, since the work of Kaneko and Locke in 2001, who resolved the conjecture for oriented graphs whose minimum out-degree is at most $6$.

The proof is partially computer-assisted: after a sequence of local reductions, the remaining finite obstruction models are eliminated by reproducible OR-Tools CP-SAT infeasibility checks.