`Compfiles/Imo1967P6.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

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1967, Problem 6

In a sports contest, there were m medals awarded on n successive days (n > 1). On the first day, one medal and 1/7 of the remaining (m − 1) medals were awarded. On the second day, two medals and 1/7 of the now remaining medals were awarded; and so on. On the n-th and last day, the remaining n medals were awarded. How many days did the contest last, and how many medals were awarded altogether?

Imports (7)

Imported by 1 file

Compfiles.lean

abbrev Imo1967P6.MedalsProcess The process described in the problem, from the point of view of the medals remaining: r k is the number of medals left at the start of day k + 1 (so r 0 = m) line 40 source
Source documentation
The process described in the problem, from the point of view of the medals remaining: r k is the number of medals left at the start of day k + 1 (so r 0 = m). On day k (for 1 ≤ k ≤ n - 1), k medals and one seventh of the rest are awarded, which has to be a whole number of medals. On the last day the remaining n medals are awarded, i.e. r (n - 1) = n.

no axioms what this means
Statement uses: Nat, Int
Proof uses: And, Eq, OfNat.ofNat, HSub.hSub, LE.le, Dvd.dvd, HAdd.hAdd, HDiv.hDiv
13 instances, coercions and auxiliary constants left out.
```
abbrev MedalsProcess (m n : ℕ) (r : ℕ → ℤ) : Prop :=
…
```
theorem Imo1967P6.rec_eq The day-k rule implies the recurrence 7 * r k = 6 * (r (k - 1) - k) line 50 source
Source documentation
The day-k rule implies the recurrence 7 * r k = 6 * (r (k - 1) - k).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Dvd.dvd, OfNat.ofNat, HSub.hSub, Eq, HAdd.hAdd, HDiv.hDiv, HMul.hMul
Proof uses: Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 50 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem rec_eq {r : ℕ → ℤ} {k : ℕ} (h7 : 7 ∣ r (k - 1) - ↑k)
    (hk : r k = r (k - 1) - (↑k + (r (k - 1) - ↑k) / 7)) :
    7 * r k = 6 * (r (k - 1) - ↑k) := by
…
```
theorem Imo1967P6.closed_form Solving the recurrence: after k days the number of remaining medals is (6/7)^k * (m - 36) + 36 - 6k line 60 source
Source documentation
Solving the recurrence: after k days the number of remaining medals is (6/7)^k * (m - 36) + 36 - 6k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Eq, OfNat.ofNat, LE.le, HSub.hSub, HMul.hMul, Rat, HAdd.hAdd, HPow.hPow, HDiv.hDiv
Proof uses: Nat.recAux, Eq.mpr, id, congrArg, congr, Int.cast_natCast, Nat.cast_zero, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr and 96 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem closed_form {m n : ℕ} {r : ℕ → ℤ} (h0 : r 0 = ↑m)
    (hrec : ∀ k, 1 ≤ k → k ≤ n - 1 → 7 * r k = 6 * (r (k - 1) - ↑k)) :
    ∀ k, k ≤ n - 1 → (r k : ℚ) = (6 / 7 : ℚ) ^ k * (↑m - 36) + 36 - 6 * ↑k := by
…
```
theorem Imo1967P6.key_eq Specializing the closed form at k = n - 1 (where r (n - 1) = n) gives the key Diophantine relation between m and n line 85 source
Source documentation
Specializing the closed form at k = n - 1 (where r (n - 1) = n) gives the key Diophantine relation between m and n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Int, Eq, HSub.hSub, LE.le, HMul.hMul, HPow.hPow
Proof uses: HAdd.hAdd, Exists, Exists.intro, Rat, HDiv.hDiv, Imo1967P6.closed_form, le_rfl, Eq.mpr, id, congrFun', congrArg, Nat.add_sub_cancel, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 99 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
theorem key_eq {m n : ℕ} (hn : 1 < n) {r : ℕ → ℤ} (h0 : r 0 = ↑m)
    (hn1 : r (n - 1) = ↑n)
    (hrec : ∀ k, 1 ≤ k → k ≤ n - 1 → 7 * r k = 6 * (r (k - 1) - ↑k)) :
    (6 : ℤ) ^ (n - 1) * (↑m - 36) = 7 ^ n * (↑n - 6) := by
…
```
theorem Imo1967P6.forward The forward direction: the Diophantine relation forces n = 6 and m = 36, because 6 ^ (n - 1) must divide n - 6 while growing much faster line 109 source
Source documentation
The forward direction: the Diophantine relation forces n = 6 and m = 36, because 6 ^ (n - 1) must divide n - 6 while growing much faster.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Int, Imo1967P6.MedalsProcess, Eq, Prod, Prod.mk
Proof uses: And, HSub.hSub, LE.le, Dvd.dvd, HAdd.hAdd, HDiv.hDiv, HMul.hMul, Imo1967P6.rec_eq, And.left, And.right, HPow.hPow, Imo1967P6.key_eq, Exists.intro, Eq.symm, Eq.mp, congrArg, congrFun', Nat.add_sub_cancel, IsCoprime, IsCoprime.pow and 104 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
theorem forward {m n : ℕ} (hn : 1 < n) (h : ∃ r : ℕ → ℤ, MedalsProcess m n r) :
    (m, n) = (36, 6) := by
…
```
Mentions: h, Imo1967P6.MedalsProcess
theorem Imo1967P6.backward The converse direction: with m = 36 and n = 6 exactly six medals are awarded on each of the six days line 152 source
Source documentation
The converse direction: with m = 36 and n = 6 exactly six medals are awarded on each of the six days.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, Int, Imo1967P6.MedalsProcess, OfNat.ofNat
Proof uses: Exists.intro, ite, LE.le, HSub.hSub, HMul.hMul, And.intro, Eq, And, Dvd.dvd, HAdd.hAdd, HDiv.hDiv, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true, eq_true, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat and 26 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem backward : ∃ r : ℕ → ℤ, MedalsProcess 36 6 r := by
…
```
Mentions: Imo1967P6.MedalsProcess
determine Imo1967P6.solution line 162 source
no axioms what this means
Statement uses: Prod, Nat
Proof uses: Prod.mk, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
problem Imo1967P6.imo1967_p6 line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Exists, Int, Imo1967P6.MedalsProcess, Eq, Prod, Prod.mk, Imo1967P6.solution
Proof uses: Iff.intro, Eq.mpr, id, congrArg, Imo1967P6.solution.eq_1, Imo1967P6.forward, And, Eq.mp, Prod.mk.injEq, Imo1967P6.backward, Eq.symm
6 instances, coercions and auxiliary constants left out.

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