AI Proved What?

Episode 162, October 2026

Ryser disproved?

Two preprints claim intersecting hypergraphs with r parts that need all r vertices to cover, one more than Ryser’s conjecture allows

Covers result 162 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

Play Episode 162: Ryser disproved? A complete graph on nine vertices with its edges in four colours, from the plane of order three (our drawing).

6:31. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The conjecture
  2. 1:44The claim
  3. 3:13How the proof goes
  4. 5:31Where it stands

The claim, in plain words

An r-partite r-uniform hypergraph has r disjoint parts, and each edge has exactly one vertex in each part (in the video: r teams, and each hyperedge picks one player from every team). A cover is a set of vertices meeting every edge; τ is the size of the smallest one, and ν the largest number of pairwise disjoint edges. Ryser’s covering conjecture “asserts that every such hypergraph satisfies τ(H) ≤ (r−1)ν(H)”. When every two edges meet (the intersecting case, ν = 1), it asks for a cover with r−1 vertices, while any single edge is a cover with r. The affine plane of order q shows why r−1 is natural: with one part per direction, one vertex per line and one edge per point, the hypergraph is intersecting and τ = q = r−1. As the papers recount, the conjecture holds for two parts by Kőnig’s theorem and for three by Aharoni, and its intersecting case through four parts (Gyárfás) and five (Tuza). Gyárfás’s conjecture, that r−1 monochromatic trees cover the vertices of any r-edge-coloured complete graph, is equivalent to the intersecting case, as Erdős, Gyárfás and Pyber record.

Result 162 rests on two OpenAI preprints. Balanced counterexamples to Ryser’s conjecture at prime orders (40 pages, dated September 27, 2026), Theorem 1.1: for every prime q beyond some threshold “there is a finite intersecting (q+1)-partite (q+1)-uniform hypergraph H with |V1| = ⋯ = |Vq+1| = q+1, τ(H) = q+1. Every vertex belongs to an edge.” A counterexample to Ryser’s covering conjecture (39 pages, dated September 23, 2026), Theorem 1.1: the same covering number q+1 for q = sn, where s ≥ s0 is a prime with s ≡ 2 (mod 3) and n ≥ n0(s) is odd, without equal part sizes. In both, τ = r is one more than predicted and the most an intersecting hypergraph can need. Both papers derive (Corollary 1.2) r-edge-coloured complete graphs that need exactly r monochromatic trees. The catalog entry credits the colouring consequence to the extension-field construction only; both papers prove it.

What it doesn’t claim

Neither paper writes a hypergraph down: each shows that a random construction succeeds with positive probability. Neither gives a number for the threshold (“that threshold is not numerical”; “the proof does not give a numerical threshold”), and some constants come from arguments by contradiction. By our rough reading of the first paper’s explicit constants, its route needs primes beyond about 101.4×1011 even with the most favourable values, and the second paper’s route needs far more; that is what the proofs need, not an estimate of the smallest counterexample. Only the ranks q+1 (q a large prime) and sn+1 are covered; two or three parts in general, and up to five in the intersecting case, remain theorems. The colouring results are about covering only: the second paper sets aside the tree-partition conjecture of Erdős, Gyárfás and Pyber. The printed dates are labels: the paper dated September 23 cites and uses lemmas from the one dated September 27, and both PDFs were compiled on October 5.

Where it stands

Posted as preprints
OpenAI, 40 and 39 pages, dated September 27 and 23, 2026
Peer reviewed
Not yet
Checked in Lean
Both main theorems exactly; the colouring corollaries are not formalized. We have not rebuilt it

Last checked October 19, 2026. Neither preprint has been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization with three comparator statements: the prime-order theorem exactly, with parts of exactly q+1 vertices, all used (comparator); the extension-field theorem exactly, plus infinitely many ranks; and a weaker fixed-prime variant. By our count the proofs take 918 files and 116,039 lines excluding Mathlib (prime-order development, extension-field development). Lean proves the case of the Szőnyi–Weiner stability theorem that the first paper uses, and, like the papers, shows the hypergraphs exist without building one. We found no unproved steps, and we have not rebuilt it. The colouring corollaries are not formalized, and the repository’s formalization list omits the first paper. Neither paper is among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Start from the plane. In the affine plane of order q every direction is a cover of size q. Both papers relabel so that no q vertices cover, while every two edges still meet.
  2. Merge and split (prime orders). In each direction, two parallel lines merge into one vertex and two others keep only four chosen points each, split into two crosswise pairs: (q−4) + 1 + 4 = q+1 vertices per part. Each neighbouring pair of chosen points lies on the two lines of a merged pair in another direction, so it still shares a vertex.
  3. No cover of size q. Setting aside split lines and one line of each merged pair leaves an ordinary covering of a large core by at most q lines. Random-deletion counting and the Szőnyi–Weiner stability theorem (“the step that requires q to be prime”) force almost all of them through one point, or all parallel; then every unsplit line through that point is forced, and the remaining budget cannot reach the chosen points. Random choices, completed with the local lemma, produce the data for large q.
  4. The extension-field route. In a plane of prime order s, delete one line of each nonzero slope and cube the first coordinate, a bijection when s ≡ 2 (mod 3); for large s and a good random choice, covering what remains with at most s lines forces a whole direction. Copies are planted in a plane of order sn, and a sum–product incidence bound, which needs every proper subfield to have order at most q1/3, forces n odd.
  5. Trees. Edges of the hypergraph become vertices of a complete graph, and a pair is coloured by a part where the two edges share a vertex; a one-colour connected piece names one vertex, so r trees are needed.

The numbers in the video

  • Our check of the plane examples: τ = q for orders 2, 3, 4, 5, 7, 8, 9; for orders 2 to 5, exhaustively, every smallest cover is a whole direction (3, 4, 5 and 6 of them). The tree versions need 2 trees for K4 with 3 colours and 3 for K9 with 4.
  • Our merge-and-split example at q = 11 (random merged pairs): the split line y = 3, chosen points x = 3, 8, 6, 10, neighbouring pairs joined by merged pairs of slopes 1, 7, 9 and 10.
  • Our gadget example at s = 11 (one random choice): 47 points remain; the cheapest line cover is 8 lines before cubing and 10 after, not yet 11, as expected for a lemma stated for large s.
  • The Lean counts: 918 files and about 116,000 lines, our count of the three import closures.

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The conjecture

Split some players into r teams. A hyperedge picks one player from every team, and suppose every two hyperedges share at least one player: the hypergraph is intersecting. A cover is a set of players that touches every hyperedge, and the covering number is the size of the smallest one. Any single hyperedge is itself a cover, so r players always suffice. Ryser’s covering conjecture predicts that r minus one are enough, and in general, that the covering number is at most r minus one times the largest number of disjoint hyperedges. The catch is that a cover may mix players from different teams. Finite planes show why r minus one is natural. Take the plane over the field with three elements: nine points, and lines in four directions. Make each direction a team and each line a player, and let each point be the hyperedge of the four lines through it. Two points always share the line joining them, and the three lines of one direction cover every point, so three players, r minus one, suffice, and fewer will not do. In our check of planes up to order five, every smallest cover is a whole direction. As the papers recount, the conjecture holds for two teams by Kőnig’s theorem and for three by Aharoni, and its intersecting case through five teams, by Gyárfás and Tuza. There is a twin question about colourings. Colour every edge of a complete graph with one of r colours, and cover its vertices with trees that each use a single colour. Gyárfás’s conjecture asks whether r minus one such trees always suffice. Erdős, Gyárfás and Pyber record that this is equivalent to the intersecting case of Ryser’s conjecture.

1:44The claim

Result 162 rests on two OpenAI preprints. The first, 40 pages, dated September 27, says: for every sufficiently large prime q, there is an intersecting hypergraph with q plus one teams, each with exactly q plus one players, whose covering number is q plus one. The prediction was q. That is one more, and q plus one is the most any intersecting hypergraph with that many teams can need. The second paper, 39 pages, dated September 23, reaches team counts of the form s to the n, plus one, where s is a large prime leaving remainder two on division by three, and n is large and odd; its teams need not be equal. Both papers derive the colouring version: some colourings with r colours need r single-colour trees. If the proofs hold, both conjectures are false. Neither paper writes a counterexample down. Each shows that a random construction succeeds with positive probability, and neither says how large the prime must be; one calls its threshold not numerical. By our rough reading of the constants, the proofs need astronomically large planes. Only these team counts are covered: other counts are not addressed, and two or three teams in general, and up to five in the intersecting case, remain theorems. The colouring consequence concerns covering only; the second paper explicitly sets aside a related conjecture about partitions into trees.

3:13How the proof goes

Both papers start from the plane example and change the labels, so that no q players cover any more, while every two hyperedges still meet. The prime-order paper does it like this. In each direction, merge two parallel lines into one player, and cut two other lines down to four chosen points each, split into two crosswise pairs. That gives q minus four, plus one, plus four: q plus one players in every direction. Splitting separates neighbouring chosen points, so the points are picked so that each neighbouring pair lies on the two merged lines of some other direction, and still shares a player there. Now suppose q players covered everything. Set aside the split lines and one line of each merged pair, and what is left is an ordinary covering of a large leftover set by at most q lines. Counting under random deletions, plus a stability theorem of Szőnyi and Weiner for planes of prime order, shows that almost all of those lines pass through one point, or are all parallel. Then every unsplit line through that point is forced into the cover, and the few players left over cannot reach all the chosen points on the split lines through it. The data exist because a random choice, completed with the local lemma, succeeds with positive probability once q is large. The other paper starts in a small plane over the field with s elements. Delete one line of each nonzero slope, chosen at random, and cube the first coordinate. When s leaves remainder two on division by three, cubing shuffles the columns without collisions and bends the sloped lines into curves, and the paper proves that, for large s and a good random choice, covering what remains with at most s lines forces a whole direction. In one random example of ours at s = 11, cubing raised the cheapest line cover from eight lines to ten, not yet to eleven. Copies of this gadget are planted in a big plane of order s to the n. An incidence bound from the sum-product method needs the big field to have no large subfield, which is why n is odd. Finally, making each hyperedge a vertex of a complete graph, and colouring each pair by a team where the two share a player, turns the counterexample into a colouring that needs r trees.

5:31Where it stands

Both papers are preprints, not peer reviewed and not revised since release. OpenAI’s Lean formalization states and proves the prime-order theorem exactly, equal team sizes included, and the extension-field theorem exactly, plus a weaker variant, in about 116,000 lines, by our count. It even proves the case of the Szőnyi and Weiner theorem that the first paper uses. We found no unproved steps, and we have not rebuilt it. Like the papers, Lean proves the hypergraphs exist without writing one down, and the colouring consequence is not formalized. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If the proofs hold, r minus one is not always enough: at infinitely many team counts, an intersecting hypergraph needs all r players. But neither paper draws one, and the smallest team count where it happens is unknown.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.