Ryser's conjecture for $r = 2$ (Kőnig's theorem)

Proved

TenChallenges.challenge_08_r2

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

hypergraphsryserten-challenges

The rung $r=2$ of Ryser's conjecture: Kőnig's theorem. Every $2$ -partite $2$ -uniform finite hypergraph, that is, every finite bipartite graph, satisfies

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

Preamble

import Definitions.Def_TenChallenges_Challenge_08
universe u

Formal statement

namespace TenChallenges
theorem challenge_08_r2 : statement_08 2 := by sorry
end TenChallenges

Source

Kőnig's theorem (1931); e.g. R. Diestel, Graph Theory, 5th ed., Theorem 2.1.1, https://doi.org/10.1007/978-3-662-53622-3

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).

View graph

Ryser's conjecture for r=2r = 2r=2 (Kőnig's theorem)

Ryser's conjecture for $r = 2$ (Kőnig's theorem)