Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2001P3

import Mathlib.Data.Set.Card
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2001, Problem 3

Twenty-one girls and twenty-one boys took part in a mathematical competition.
It turned out that each contestant solved at most six problems, and for each
pair of a girl and a boy, there was at most one problem solved by both the
girl and the boy. Show that there was a problem solved by at least three
girls and at least three boys.
-/

namespace Imo2001P3

theorem imo2001_p3 {Girl Boy Problem : Type}
    [Finite Girl] [Finite Boy] [Finite Problem]
    (girl_card : Nat.card Girl = 21)
    (boy_card : Nat.card Boy = 21)
    (girl_solved : Girl → Problem → Prop)
    (boy_solved : Boy → Problem → Prop)
    (hG : ∀ g : Girl, Set.ncard {p | girl_solved g p} ≤ 6)
    (hB : ∀ b : Boy, Set.ncard {p | boy_solved b p} ≤ 6)
    (hp : ∀ g : Girl, ∀ b : Boy, Set.ncard {p | girl_solved g p ∧ boy_solved b p} ≤ 1)
    : ∃ p : Problem, 3 ≤ Set.ncard {g | girl_solved g p} ∧
                     3 ≤ Set.ncard {g | boy_solved g p} := sorry


end Imo2001P3

File author(s): David Renshaw

This problem does not yet have a complete formalized solution.