Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1996P1

module

public import Mathlib.Tactic

public section


/-!
# International Mathematical Olympiad 1996, Problem 1

We are given a positive integer r and a rectangular board ABCD with
dimensions |AB| = 20, |BC| = 12. The rectangle is divided into a grid of
20 × 12 unit squares. The following moves are permitted on the board:
one can move from one square to another only if the distance between the
centers of the two squares is √r. The task is to find a sequence of moves
leading from the square with A as a vertex to the square with B as
a vertex.

(a) Show that the task cannot be done if r is divisible by 2 or 3.
(b) Prove that the task is possible when r = 73.
(c) Can the task be done when r = 97?
-/

namespace Imo1996P1

/- We identify each unit square with the integer coordinates `(i, j)` of its
center: `i` is the column in the direction from `A` to `B` and `j` is the row,
so `1 ≤ i ≤ 20` and `1 ≤ j ≤ 12`. The square with vertex `A` is `(1, 1)` and
the square with vertex `B` is `(20, 1)`. The centers of two squares differ by
an integer vector `(a, b)`, and the distance between the centers is
`√(a² + b²)`, so a move between them is permitted exactly when `a² + b² = r`. -/

/-- The predicate that `p` is a square of the 20 × 12 board. -/
abbrev OnBoard (p : ℤ × ℤ) : Prop := 1 ≤ p.1 ∧ p.1 ≤ 20 ∧ 1 ≤ p.2 ∧ p.2 ≤ 12

/-- A permitted move between two squares: both lie on the board and the
squared distance between their centers equals `r`. -/
abbrev Move (r : ℤ) (p q : ℤ × ℤ) : Prop :=
  OnBoard p ∧ OnBoard q ∧ (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 = r

/-- The square with vertex `A`. -/
abbrev SqA : ℤ × ℤ := (1, 1)

/-- The square with vertex `B`. -/
abbrev SqB : ℤ × ℤ := (20, 1)

theorem imo1996_p1_a (r : ℤ) (hr : 2 ∣ r ∨ 3 ∣ r) :
    ¬ Relation.ReflTransGen (Move r) SqA SqB := sorry

theorem imo1996_p1_b : Relation.ReflTransGen (Move 73) SqA SqB := sorry

/- determine -/ abbrev does_exist_97 : Bool := sorry

theorem imo1996_p1_c :
    if does_exist_97 then Relation.ReflTransGen (Move 97) SqA SqB
    else ¬ Relation.ReflTransGen (Move 97) SqA SqB := sorry

end Imo1996P1

File author(s): Kimi K3

This problem has a complete formalized solution.