Documentation

Archive.Imo.Imo2001Q3

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 21Finset ) :

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.

Instances For
    def Imo2001Q3.Easy (F : Fin 21Finset ) (p : ) :

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

    Equations
    Instances For
      theorem Imo2001Q3.card_not_easy_le_five {G B : Fin 21Finset } {i : Fin 21} (hG : (G i).card 6) (hB : ∀ (j : Fin 21), ¬Disjoint (G i) (B j)) :
      {pG 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 21Finset } (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 21Finset } (h : Condition G B) :
      ∃ (p : ), Easy G p Easy B p