`Compfiles/Imo1996P1.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

20 declarations, 0 contain sorry, 0 declared as axioms

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?

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo1996P1.OnBoard The predicate that p is a square of the 20 × 12 board line 42 source
Source documentation
The predicate that p is a square of the 20 × 12 board.

no axioms what this means
Statement uses: Prod, Int
Proof uses: And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd
2 instances, coercions and auxiliary constants left out.
```
abbrev OnBoard (p : ℤ × ℤ) : Prop := 1 ≤ p.1 ∧ p.1 ≤ 20 ∧ 1 ≤ p.2 ∧ p.2 ≤ 12
```
abbrev Imo1996P1.Move A permitted move between two squares: both lie on the board and the squared distance between their centers equals r line 46 source
Source documentation
A permitted move between two squares: both lie on the board and the squared distance between their centers equals r.

standard axioms: propext what this means
Statement uses: Int, Prod
Proof uses: And, Imo1996P1.OnBoard, Eq, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Prod.fst, OfNat.ofNat, Prod.snd
9 instances, coercions and auxiliary constants left out.
```
abbrev Move (r : ℤ) (p q : ℤ × ℤ) : Prop :=
…
```
abbrev Imo1996P1.SqA The square with vertex A line 50 source
Source documentation
The square with vertex A.

no axioms what this means
Statement uses: Prod, Int
Proof uses: Prod.mk, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev SqA : ℤ × ℤ := (1, 1)
```
abbrev Imo1996P1.SqB The square with vertex B line 53 source
Source documentation
The square with vertex B.

no axioms what this means
Statement uses: Prod, Int
Proof uses: Prod.mk, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev SqB : ℤ × ℤ := (20, 1)
…
```
lemma Imo1996P1.sq_mod_two line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HMod.hMod, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Even, Odd, Or, Int.even_or_odd, HAdd.hAdd, HMul.hMul, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_overlap, Mathlib.Tactic.Ring.Common.add_overlap_pf, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 34 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.sq_mod_three line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Or, Eq, HMod.hMod, HPow.hPow, Nat, OfNat.ofNat
Proof uses: HAdd.hAdd, HMul.hMul, Exists, Exists.intro, HDiv.hDiv, Or.inl, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 36 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.sq_mod_three_eq_zero line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HMod.hMod, HPow.hPow, Nat, OfNat.ofNat
Proof uses: Or, HAdd.hAdd, HMul.hMul, Exists, Exists.intro, HDiv.hDiv, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm and 28 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.step_two If r is even and a² + b² = r, then a ≡ b (mod 2), so a move preserves the parity of p.1 + p.2 line 94 source
Source documentation
If r is even and a² + b² = r, then a ≡ b (mod 2), so a move preserves the parity of p.1 + p.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Dvd.dvd, OfNat.ofNat, Prod, Imo1996P1.Move, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Prod.snd
Proof uses: Imo1996P1.OnBoard, And, HPow.hPow, Nat, HSub.hSub, HMul.hMul, Imo1996P1.sq_mod_two
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma step_two {r : ℤ} (hr : 2 ∣ r) {p q : ℤ × ℤ} (h : Move r p q) :
    (p.1 + p.2) % 2 = 0 → (q.1 + q.2) % 2 = 0 := by
…
```
Mentions: h, Imo1996P1.Move
lemma Imo1996P1.step_three If 3 ∣ r and a² + b² = r, then 3 ∣ a and 3 ∣ b, so a move preserves p.1 mod 3 line 104 source
Source documentation
If 3 ∣ r and a² + b² = r, then 3 ∣ a and 3 ∣ b, so a move preserves p.1 mod 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Dvd.dvd, OfNat.ofNat, Prod, Imo1996P1.Move, Eq, HMod.hMod, Prod.fst
Proof uses: Imo1996P1.OnBoard, And, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Prod.snd, HMul.hMul, Or, Imo1996P1.sq_mod_three, Imo1996P1.sq_mod_three_eq_zero
24 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma step_three {r : ℤ} (hr : 3 ∣ r) {p q : ℤ × ℤ} (h : Move r p q) :
    p.1 % 3 = 1 → q.1 % 3 = 1 := by
…
```
Mentions: h, Imo1996P1.Move
lemma Imo1996P1.reach_two line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Dvd.dvd, OfNat.ofNat, Prod, Relation.ReflTransGen, Imo1996P1.Move, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Prod.snd
Proof uses: Relation.ReflTransGen.rec, id, Imo1996P1.step_two
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.reach_three line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Dvd.dvd, OfNat.ofNat, Prod, Relation.ReflTransGen, Imo1996P1.Move, Eq, HMod.hMod, Prod.fst
Proof uses: Relation.ReflTransGen.rec, id, Imo1996P1.step_three
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.abs_le_nine line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, LE.le, abs
Proof uses: Decidable.byContradiction, Not, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 72 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.sq97_aux line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HPow.hPow, Nat, Or, And
Proof uses: dite, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Not, HSub.hSub, Int.le_sub_one_of_not_le, Mathlib.Tactic.IntervalCases.of_le_left
126 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1996P1.move97 The only ways to write 97 as a sum of two squares are 81 + 16 and 16 + 81, so each permitted move for r = 97 is of the form (±9, ±4) or (±4, ±9) line 149 source
Source documentation
The only ways to write 97 as a sum of two squares are 81 + 16 and 16 + 81, so each permitted move for r = 97 is of the form (±9, ±4) or (±4, ±9).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, Or, And, abs
Proof uses: LE.le, Imo1996P1.abs_le_nine, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, HMul.hMul, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.neg_congr and 56 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma move97 {a b : ℤ} (h : a ^ 2 + b ^ 2 = 97) :
    (|a| = 9 ∧ |b| = 4) ∨ (|a| = 4 ∧ |b| = 9) := by
…
```
Mentions: h
lemma Imo1996P1.step97 The invariant for part (c): row membership in the central strip {5, 6, 7, 8} agrees with evenness of the column line 161 source
Source documentation
The invariant for part (c): row membership in the central strip {5, 6, 7, 8} agrees with evenness of the column. A "toggle" move (±9, ±4) flips both sides of the equivalence; a move (±4, ±9) flips neither (such a move cannot start or end inside the strip, and it preserves the parity of the column).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Imo1996P1.Move, OfNat.ofNat, Iff, Eq, HMod.hMod, Prod.fst, And, LE.le, Prod.snd
Proof uses: Imo1996P1.OnBoard, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Or, abs, Imo1996P1.move97, Neg.neg, eq_or_eq_neg_of_abs_eq
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma step97 {p q : ℤ × ℤ} (h : Move 97 p q) :
    (p.1 % 2 = 0 ↔ 5 ≤ p.2 ∧ p.2 ≤ 8) → (q.1 % 2 = 0 ↔ 5 ≤ q.2 ∧ q.2 ≤ 8) := by
…
```
Mentions: h, Imo1996P1.Move
lemma Imo1996P1.reach97 line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Prod, Int, Relation.ReflTransGen, Imo1996P1.Move, OfNat.ofNat, Iff, Eq, HMod.hMod, Prod.fst, And, LE.le, Prod.snd
Proof uses: Relation.ReflTransGen.rec, id, Imo1996P1.step97
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
problem Imo1996P1.imo1996_p1_a line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Or, Dvd.dvd, OfNat.ofNat, Not, Relation.ReflTransGen, Prod, Imo1996P1.Move, Imo1996P1.SqA, Imo1996P1.SqB
Proof uses: False, absurd, Eq, HMod.hMod, HAdd.hAdd, Prod.fst, Prod.snd, Imo1996P1.reach_two, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Imo1996P1.reach_three
11 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
problem Imo1996P1.imo1996_p1_b line 187 source
standard axioms: propext what this means
Statement uses: Relation.ReflTransGen, Prod, Int, Imo1996P1.Move, OfNat.ofNat, Imo1996P1.SqA, Imo1996P1.SqB
Proof uses: Prod.mk, And.intro, Imo1996P1.OnBoard, And, Eq, HAdd.hAdd, HPow.hPow, Nat, HSub.hSub, Prod.fst, Prod.snd, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl, Relation.ReflTransGen.head, Relation.ReflTransGen.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
determine Imo1996P1.does_exist_97 line 207 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.false
problem Imo1996P1.imo1996_p1_c line 209 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ite, Eq, Bool, Imo1996P1.does_exist_97, Bool.true, Relation.ReflTransGen, Prod, Int, Imo1996P1.Move, OfNat.ofNat, Imo1996P1.SqA, Imo1996P1.SqB, Not
Proof uses: id, absurd, Iff, HMod.hMod, Prod.fst, And, LE.le, Prod.snd, False, Imo1996P1.reach97, of_decide_eq_true, Decidable.decide, Eq.refl
12 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.