Ryser's conjecture for $r = 4$

Open

TenChallenges.challenge_08_r4

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

hypergraphsryserten-challenges

The rung $r=4$ of Ryser's conjecture. Every $4$ -partite $4$ -uniform finite hypergraph satisfies

\tau(\mathcal H)\ \le\ 3\,\nu(\mathcal H).

This rung is open.

Preamble

import Definitions.Def_TenChallenges_Challenge_08
universe u

Formal statement

namespace TenChallenges
theorem challenge_08_r4 : statement_08 4 := by sorry
end TenChallenges

Source

Open; partial result

\tau\le(4-\varepsilon)\nu

in P. E. Haxell, A. D. Scott, On Ryser's conjecture, Electron. J. Combin. 19 (2012), P23, https://doi.org/10.37236/1175

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

Ryser's conjecture for r=4r = 4r=4