Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1988P2

import Mathlib

/-!
# International Mathematical Olympiad 1988, Problem 2

Let n be a positive integer and let A₁, A₂, ..., A₂ₙ₊₁ be subsets
of a set B. Suppose that

(i) each Aᵢ has exactly 2n elements,
(ii) each intersection Aᵢ ∩ Aⱼ (i ≠ j) contains exactly one element, and
(iii) every element of B belongs to at least two of the Aᵢ.

For which values of n can one assign to every element of B
one of the numbers 0 and 1 in such a way that each Aᵢ has
exactly n elements assigned 0?
-/

namespace Imo1988P2

/- determine -/ abbrev SolutionSet : Set ℕ := sorry

theorem imo1988_p2 (n : ℕ) :
    n ∈ SolutionSet ↔
    (0 < n ∧
     ∀ (B : Type) [DecidableEq B] (A : Fin (2 * n + 1) → Finset B),
       (∀ i, (A i).card = 2 * n) →
       (∀ i j, i ≠ j → (A i ∩ A j).card = 1) →
       (∀ b : B, 2 ≤ (Finset.univ.filter (fun i ↦ b ∈ A i)).card) →
       ∃ f : B → Fin 2, ∀ i, ((A i).filter (fun b ↦ f b = 0)).card = n) := sorry

end Imo1988P2

This problem has a complete formalized solution.