Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2005P6

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Combinatorics.Enumerative.DoubleCounting
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.ModEq
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.Ring

public section


/-!
# International Mathematical Olympiad 2005, Problem 6

In a mathematical competition 6 problems were posed to the contestants. Each
pair of problems was solved by more than 2/5 of the contestants. Nobody solved
all 6 problems. Show that there were at least 2 contestants who each solved
exactly 5 problems.
-/

namespace Imo2005P6

open Finset

theorem imo2005_p6 {n : ℕ} (s : Fin n → Finset (Fin 6))
    (pair : ∀ p q : Fin 6, p ≠ q →
      2 * n < 5 * (Finset.univ.filter fun i => p ∈ s i ∧ q ∈ s i).card)
    (hall : ∀ i, (s i).card < 6) :
    ∃ i j, i ≠ j ∧ (s i).card = 5 ∧ (s j).card = 5 := sorry

end Imo2005P6

File author(s): Kimi K3

This problem has a complete formalized solution.