Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1974P1


import Mathlib

/-!

# International Mathematical Olympiad 1974, Problem 1

Three players $A, B$ and $C$ play the following game:

* On each of three cards an integer is written.
* These three numbers $p, q, r$ satisfy $0 < p < q < r$.
* The three cards are shuffled and one is dealt to each player.
* Each then receives the number of counters indicated by the card he holds.
* Then the cards are shuffled again; the counters remain with the players.

This process (shuffling, dealing, giving out counters) takes place
for at least two rounds. After the last round, $A$ has 20 counters in all,
$B$ has 10 and $C$ has 9. At the last round $B$ received $r$ counters.

Who received $q$ counters on the first round?
-/

namespace Imo1974P1

abbrev Player := Fin 3

/- determine -/ abbrev solution : Player := sorry  -- player C

theorem imo1974_p1
  (p q r : ℕ)
  (hpqr : 0 < p ∧ p < q ∧ q < r)
  (n : ℕ)
  (hn : 1 < n)
  (game : ℕ → (Player ≃ Fin 3))
  (hA : ∑ k ∈ Finset.range n, ![p,q,r] (game k 0) = 20)
  (hB : ∑ k ∈ Finset.range n, ![p,q,r] (game k 1) = 10)
  (hC : ∑ k ∈ Finset.range n, ![p,q,r] (game k 2) = 9)
  (hl : ![p,q,r] (game (n-1) 1) = r)
  : game 0 solution = 1 := sorry

end Imo1974P1

File author(s): Lynn Van Hauwe

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org:
External resources: