# Counterexamples to Ryser’s covering conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Balanced counterexamples to Ryser's conjecture at prime orders](../../preprints/Balanced-Counterexamples-to-Rysers-Conjecture-at-Prime-Orders-September-27-2026/paper.pdf)
- [A counterexample to Ryser's covering conjecture](../../preprints/A-Counterexample-to-Rysers-Covering-Conjecture-September-23-2026/paper.pdf)

## Scope

Ryser's covering conjecture predicts that an intersecting $r$-partite hypergraph has a vertex cover of size at most $r-1$. The formalization proves that every sufficiently large prime $q$ has a finite intersecting $(q+1)$-partite, $(q+1)$-uniform hypergraph with covering number $q+1$ and exactly $q+1$ nonisolated vertices in each part. Thus the conjecture fails even with equal part sizes. The prime threshold is existential.

Ryser's covering conjecture predicts $\tau\le(r-1)\nu$ for an $r$-partite hypergraph, where $\tau$ and $\nu$ are its covering and matching numbers. The formalized constructions give finite intersecting $r$-partite $r$-uniform hypergraphs with $\nu=1$ and $\tau=r$, contradicting the bound. The ranks have the form $r=p^n+1$: one fixed prime $p\equiv2\pmod3$ works for all sufficiently large prime degrees $n$, and a second result covers every sufficiently large such prime $p$ and every sufficiently large odd $n$, with the degree threshold allowed to depend on $p$. Infinitely many ranks occur. Equal part sizes and numerical thresholds are not asserted.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Balanced Ryser counterexamples at prime orders | [BalancedRyser.lean](../ComparatorChallenges/BalancedRyser.lean) |
| Fixed-prime Ryser counterexamples | [RyserCovering.lean](../ComparatorChallenges/RyserCovering.lean) |
| Counterexamples in odd extension degrees | [RyserOddExtensions.lean](../ComparatorChallenges/RyserOddExtensions.lean) |