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

15 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2010, Problem 5

Each of the six boxes $B_1, B_2, B_3, B_4, B_5, B_6$ initially contains one coin. The following two types of operations are allowed:

Choose a non-empty box $B_j, 1 ≤ j ≤ 5$, remove one coin from $B_j$ and add two coins to $B_{j+1}$;
Choose a non-empty box $B_k, 1 ≤ k ≤ 4$, remove one coin from $B_k$ and swap the contents (possibly empty) of the boxes $B_{k+1}$ and $B_{k+2}$.

Determine if there exists a finite sequence of operations of the allowed types, such that the five boxes $B_1, B_2, B_3, B_4, B_5$ become empty, while box $B_6$ contains exactly $2010^{2010^{2010}}$ coins.

Imports (7)

Imported by 1 file

Compfiles.lean

inductive Imo2010P5.Reachable The predicate defining states of boxes reachable by the given moves line 45 source

Source documentation

The predicate defining states of boxes reachable by the given moves.

standard axioms: Classical.choice, Quot.sound, propext what this means

Statement uses: Fin, OfNat.ofNat, Nat

1 instances, coercions and auxiliary constants left out.

inductive Reachable : (Fin 6 → ℕ) → Prop
  /-- The starting position with one coin in each box -/
  | base : Reachable 1
  /-- Remove a coin from $B_j$ and add two coins to $B_{j+1}$ -/
  | move1 {B i} (rB : Reachable B) (hi : i < 5) (pB : 0 < B i) :
      Reachable (B - single i 1 + single (i + 1) 2)
  /-- Remove a coin from $B_k$ and swap $B_{k+1}$ and $B_{k+2}$ -/
  | move2 {B i} (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) :
      Reachable (B ∘ swap (i + 1) (i + 2) - single i 1)

snip begin

Mentions: base

lemma Imo2010P5.single_succ line 84 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Pi.single, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Pi.single_eq_of_ne, Not, False, not_false_eq_true, eq_self
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2010P5.single_succ' line 86 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Pi.single, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Pi.single_eq_of_ne, Not, False, not_false_eq_true, eq_self
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2010P5.single_add_two line 88 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, Pi.single, HAdd.hAdd
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Pi.single_eq_of_ne, Not, False, eq_false_of_decide, Eq.refl, Bool, Bool.false, not_false_eq_true, eq_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2010P5.Reachable.push Empty $B_i$ and add twice its coins to $B_{i+1}$ by repeatedly applying move 1 line 93 source
Source documentation
Empty $B_i$ and add twice its coins to $B_{i+1}$ by repeatedly applying move 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2010P5.Reachable, LT.lt, HAdd.hAdd, HSub.hSub, Pi.single, HMul.hMul
Proof uses: PSigma.mk
21 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma push {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 5) :
    Reachable (B - single i (B i) + single (i + 1) (2 * B i)) := by
…
```
Mentions: Imo2010P5.Reachable
lemma Imo2010P5.Reachable.five_eleven (0, 0, 5, 11, 0, 0) is reachable line 109 source
Source documentation
(0, 0, 5, 11, 0, 0) is reachable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Imo2010P5.Reachable, HAdd.hAdd, Fin, OfNat.ofNat, Nat, Pi.single
Proof uses: Eq.mpr, HSub.hSub, HMul.hMul, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Imo2010P5.Reachable.push, Imo2010P5.Reachable.base, LT.lt, Imo2010P5.Reachable.move1, Function.comp, Equiv.Perm and 2 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma five_eleven : Reachable (single 2 5 + single 3 11) := by
…
```
Mentions: Imo2010P5.Reachable
lemma Imo2010P5.Reachable.double Decrement $B_i$ and double $B_{i+1}$, assuming $B_{i+2} = 0$, by doing push, move2 line 129 source
Source documentation
Decrement $B_i$ and double $B_{i+1}$, assuming $B_{i+2} = 0$, by doing push, move2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2010P5.Reachable, LT.lt, Eq, HAdd.hAdd, HSub.hSub, Pi.single
Proof uses: Eq.mpr, Function.comp, HMul.hMul, Equiv.Perm, Equiv.swap, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HSub, funext, id, Ne, Or, eq_or_ne, congrArg, Equiv.swap_apply_of_ne_of_ne, of_eq_true and 20 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma double {B : Fin 6 → ℕ} {i : Fin 6}
    (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 2) = 0) :
    Reachable (B + single (i + 1) (B (i + 1)) - single i 1) := by
…
```
Mentions: Imo2010P5.Reachable
lemma Imo2010P5.Reachable.doubles double as many times as possible, emptying $B_i$ and doubling $B_{i+1}$ that many times line 148 source
Source documentation
double as many times as possible, emptying $B_i$ and doubling $B_{i+1}$ that many times.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2010P5.Reachable, LT.lt, Eq, HAdd.hAdd, Function.update, HSub.hSub, Pi.single, HMul.hMul, HPow.hPow
Proof uses: PSigma.mk, PSigma
25 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma doubles {B : Fin 6 → ℕ} {i : Fin 6} (rB : Reachable B) (hi : i < 4) (zB : B (i + 2) = 0) :
    Reachable (update (B - single i (B i)) (i + 1) (B (i + 1) * 2 ^ B i)) := by
…
```
Mentions: Imo2010P5.Reachable
lemma Imo2010P5.Reachable.exp Empty $B_i$ and set $B_{i+1} = 2^{B_i}$, assuming $B_{i+1} = B_{i+2} = 0$ line 167 source
Source documentation
Empty $B_i$ and set $B_{i+1} = 2^{B_i}$, assuming $B_{i+1} = B_{i+2} = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Imo2010P5.Reachable, LT.lt, Eq, HAdd.hAdd, HSub.hSub, Pi.single, HPow.hPow
Proof uses: Eq.mpr, Function.update, HMul.hMul, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, id, congrArg, congr, congrFun', Pi.single_eq_same, Imo2010P5.single_succ, Imo2010P5.single_succ', zero_tsub, zero_add, add_zero, Nat.sub_add_cancel, Nat.succ and 23 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma exp {B : Fin 6 → ℕ} {i : Fin 6}
    (rB : Reachable B) (hi : i < 4) (pB : 0 < B i) (zB : B (i + 1) = 0) (zB' : B (i + 2) = 0) :
    Reachable (B - single i (B i) + single (i + 1) (2 ^ B i)) := by
…
```
Mentions: Imo2010P5.Reachable
lemma Imo2010P5.Reachable.exp_mid From (0, 0, k+1, n, 0, 0) with n > 0 we can reach (0, 0, k, 2^n, 0, 0) line 185 source
Source documentation
From (0, 0, k+1, n, 0, 0) with n > 0 we can reach (0, 0, k, 2^n, 0, 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2010P5.Reachable, HAdd.hAdd, Fin, OfNat.ofNat, Pi.single, LT.lt, HPow.hPow
Proof uses: HSub.hSub, Imo2010P5.Reachable.exp, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, of_eq_true, Eq.trans, True, congrArg, congr, Pi.single_eq_of_ne, Not, False, eq_false_of_decide, Bool.false, not_false_eq_true and 28 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma exp_mid {k n : ℕ} (h : Reachable (single 2 (k + 1) + single 3 n)) (hn : 0 < n) :
    Reachable (single 2 k + single 3 (2 ^ n)) := by
…
```
Mentions: h, Imo2010P5.Reachable
lemma Imo2010P5.Reachable.reduce If all coins are in box 4, their number can be reduced by any desired amount line 209 source
Source documentation
If all coins are in box 4, their number can be reduced by any desired amount.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2010P5.Reachable, Pi.single, Fin, OfNat.ofNat, LE.le
Proof uses: Nat.le_induction, HAdd.hAdd, Eq.mpr, HSub.hSub, Function.comp, Equiv.Perm, Equiv.swap, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, id, Ne, Or, eq_or_ne, congrArg, Equiv.swap_apply_of_ne_of_ne and 24 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma reduce {m n : ℕ} (h : Reachable (single 3 n)) (hmn : m ≤ n) : Reachable (single 3 m) := by
…
```
Mentions: h, Imo2010P5.Reachable
lemma Imo2010P5.Reachable.tower_inequality The key power tower inequality in the solution line 223 source
Source documentation
The key power tower inequality in the solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, LE.le, HPow.hPow
Proof uses: Trans.trans, HMul.hMul, Eq.mpr, id, congrArg, pow_mul, pow_le_pow_left₀, Nat.pow_le_pow_right, Nat.zero_lt_two, HAdd.hAdd, pow_add, mul_le_mul'
40 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma tower_inequality {m n : ℕ} (hm : m = 2010) (hn : n = 11) :
    2010 ^ 2010 ^ m ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ n := by
…
```
lemma Imo2010P5.Reachable.quarter_target (0, 0, 0, 2010 ^ 2010 ^ 2010 / 4, 0, 0) is reachable line 238 source
Source documentation
(0, 0, 0, 2010 ^ 2010 ^ 2010 / 4, 0, 0) is reachable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, OfNat.ofNat, Imo2010P5.Reachable, Pi.single, Fin, HDiv.hDiv, HPow.hPow
Proof uses: HAdd.hAdd, Imo2010P5.Reachable.exp_mid, Imo2010P5.Reachable.five_eleven, Eq.mp, congrArg, rfl, Nat.two_pow_pos, Imo2010P5.Reachable.reduce, zero_add, Pi.single_zero, LE.le.trans, Nat.div_le_self, Imo2010P5.Reachable.tower_inequality
37 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma quarter_target {m : ℕ} (hm : m = 2010) : Reachable (single 3 (2010 ^ 2010 ^ m / 4)) := by
…
```
Mentions: Imo2010P5.Reachable
determine Imo2010P5.solution line 249 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.true
problem Imo2010P5.imo2010_p5 line 251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, Imo2010P5.Reachable, Pi.single, Fin, OfNat.ofNat, Nat, HPow.hPow, Eq, Bool, Imo2010P5.solution, Bool.true
Proof uses: Eq.mpr, id, Eq.trans, True, congrArg, eq_self, iff_true, rfl, Eq.refl, HAdd.hAdd, HSub.hSub, HDiv.hDiv, HMul.hMul, eq_of_heq, HEq, HEq.refl, Eq.symm, congr, Pi.single_eq_same, tsub_self and 16 more
71 instances, coercions and auxiliary constants left out.

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