Ryser's conjecture for $r = 3$ (Aharoni)

Open

TenChallenges.challenge_08_r3

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

hypergraphsryserten-challenges

The rung $r=3$ of Ryser's conjecture: Aharoni's theorem. Every $3$ -partite $3$ -uniform finite hypergraph satisfies

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

Preamble

import Definitions.Def_TenChallenges_Challenge_08
universe u

Formal statement

namespace TenChallenges
theorem challenge_08_r3 : statement_08 3 := by sorry
end TenChallenges

Source

R. Aharoni, Ryser's conjecture for tripartite 3-graphs, Combinatorica 21 (2001), 1–4, https://doi.org/10.1007/s004930170001, Theorem 1.1

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=3r = 3r=3 (Aharoni)