IMO 2001 Q3

Twenty-one girls and twenty-one boys took part in a mathematical competition. It turned out that

1. each contestant solved at most six problems, and
2. for each pair of a girl and a boy, there was at least one problem that was solved by both the girl and the boy.

Show that there is a problem that was solved by at least three girls and at least three boys.

Solution

Note that not all of the problems a girl $g$ solves can be "hard" for boys, in the sense that at most two boys solved it. If that was true, by condition 1 at most $6 × 2 = 12$ boys solved some problem $g$, but by condition 2 that property holds for all 21 boys, which is a contradiction.

Hence there are at most 5 problems $g$ solved that are hard for boys, and the number of girl-boy pairs who solved some problem in common that was hard for boys is at most $5 × 2 × 21 = 210$. By the same reasoning this bound holds when "girls" and "boys" are swapped throughout, but there are $21^2$ girl-boy pairs in all and $21^2 > 210 + 210$, so some girl-boy pairs solved only problems in common that were not hard for girls or boys. By condition 2 the result follows.

structure Imo2001Q3.Condition (G B : Fin 21 → Finset ℕ) : Prop

The conditions on the problems the girls and boys solved, represented as functions from Fin 21 (index in cohort) to the finset of problems they solved (numbered arbitrarily).

• G_le_6 (i : Fin 21) : (G i).card ≤ 6

  Every girl solved at most six problems.

• B_le_6 (j : Fin 21) : (B j).card ≤ 6

  Every boy solved at most six problems.

• G_inter_B (i j : Fin 21) : ¬Disjoint (G i) (B j)

  Every girl-boy pair solved at least one problem in common.

def Imo2001Q3.Easy (F : Fin 21 → Finset ℕ) (p : ℕ) : Prop

A problem is easy for a cohort (boys or girls) if at least three of its members solved it.

Equations

• Imo2001Q3.Easy F p = (3 ≤ {i : Fin 21 | p ∈ F i}.card)

theorem Imo2001Q3.card_not_easy_le_five {G B : Fin 21 → Finset ℕ} {i : Fin 21} (hG : (G i).card ≤ 6) (hB : ∀ (j : Fin 21), ¬Disjoint (G i) (B j)) : {p ∈ G i | ¬Easy B p}.card ≤ 5

Every contestant solved at most five problems that were not easy for the other cohort.

theorem Imo2001Q3.card_not_easy_le_210 {G B : Fin 21 → Finset ℕ} (hG : ∀ (i : Fin 21), (G i).card ≤ 6) (hB : ∀ (i j : Fin 21), ¬Disjoint (G i) (B j)) : {ij : Fin 21 × Fin 21 | ∃ (p : ℕ), ¬Easy B p ∧ p ∈ G ij.1 ∩ B ij.2}.card ≤ 210

There are at most 210 girl-boy pairs who solved some problem in common that was not easy for a fixed cohort.

theorem Imo2001Q3.result {G B : Fin 21 → Finset ℕ} (h : Condition G B) : ∃ (p : ℕ), Easy G p ∧ Easy B p