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

11 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2008, Problem 5

Let n and k be positive integers with k ≥ n and k - n an even number. There are 2n lamps labelled 1, 2, ..., 2n each of which can be either on or off. Initially all the lamps are off. We consider sequences of steps: at each step one of the lamps is switched (from on to off or from off to on). Let N be the number of such sequences consisting of k steps and resulting in the state where lamps 1 through n are all on, and lamps n + 1 through 2n are all off. Let M be the number of such sequences consisting of k steps, resulting in the state where lamps 1 through n are all on, and lamps n + 1 through 2n are all off, but where none of the lamps n + 1 through 2n is ever switched on.

Determine N/M.

Imports (3)

Imported by 1 file

Compfiles.lean

abbrev Imo2008P5.Sequence line 37 source
no axioms what this means
Statement uses: Nat
Proof uses: Fin, HMul.hMul, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
abbrev Imo2008P5.NSequence line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2008P5.Sequence
Proof uses: And, LT.lt, Odd, Nat.card, Fin, Set.ofPred, Eq, HMul.hMul, OfNat.ofNat, LE.le, Even
9 instances, coercions and auxiliary constants left out.
abbrev Imo2008P5.MSequence line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Imo2008P5.Sequence
Proof uses: And, Imo2008P5.NSequence, Fin, HMul.hMul, OfNat.ofNat, LE.le, Ne
5 instances, coercions and auxiliary constants left out.
lemma Imo2008P5.fiber_ncard_of_mod_n If g reduces f mod n (mapping [0,n) to itself and [n,2n) to [0,n) by subtracting n), then the fiber of g at i < n is the disjoint union of the fibers of f at i and n+i line 59 source
Source documentation
If g reduces f mod n (mapping [0,n) to itself and [n,2n) to [0,n) by subtracting n), then the fiber of g at i < n is the disjoint union of the fibers of f at i and n+i.
```
private lemma fiber_ncard_of_mod_n {n k : ℕ} {f g : Fin k → Fin (2 * n)}
    (hg : ∀ j, (g j).val = if (f j).val < n then (f j).val else (f j).val - n)
    (i : ℕ) (hi : i < n) :
    Set.ncard {j | (g j).val = i} =
      Set.ncard {j | (f j).val = i} + Set.ncard {j | (f j).val = n + i} := by
…
```
Mentions: f
def Imo2008P5.ψ line 71 source
lemma Imo2008P5.symmDiff_singleton_card_parity line 106 source
lemma Imo2008P5.even_subsets_card line 120 source
lemma Imo2008P5.claim line 155 source
lemma Imo2008P5.lemma1 line 398 source
determine Imo2008P5.solution line 425 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: HPow.hPow, OfNat.ofNat, HSub.hSub
5 instances, coercions and auxiliary constants left out.
problem Imo2008P5.imo2008_p5 line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Even, HSub.hSub, Eq, Rat, HMul.hMul, Set.ncard, Imo2008P5.Sequence, Imo2008P5.MSequence, Imo2008P5.solution, Imo2008P5.NSequence
Proof uses: Set.Finite, Set.ofPred, Set.toFinite, Fin, Membership.mem, Set, HPow.hPow, Eq.mpr, id, congrArg, Eq.symm, Eq.trans, Nat.cast_mul, Nat.cast_pow, Eq.refl
45 instances, coercions and auxiliary constants left out.

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