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

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2001, Problem 4

Let $n > 1$ be an odd integer and let $c_1, c_2, \dots, c_n$ be integers. For each permutation $a = (a_1, a_2, \dots, a_n)$ of $\{1, 2, \dots, n\}$, define $S(a) = \sum_{i=1}^n c_i a_i$. Prove that there exist two permutations $a ≠ b$ of $\{1, 2, \dots, n\}$ such that $n!$ is a divisor of $S(a) - S(b)$.

Imports (6)

Imported by 1 file

Compfiles.lean

def Imo2001Q4.S The function S in the problem line 44 source
Source documentation
The function S in the problem. As implemented here it accepts a permutation of Fin n rather than Icc 1 n, and as such contains + 1 to compensate.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Equiv.Perm
Proof uses: Finset.sum, Finset.univ, HMul.hMul, HAdd.hAdd, OfNat.ofNat
13 instances, coercions and auxiliary constants left out.
```
def S (c : Fin n → ℤ) (a : Perm (Fin n)) : ℤ := ∑ i, c i * (a i + 1)
…
```
lemma Imo2001Q4.sum_range_modEq_sum_of_contra Assuming the opposite of what is to be proved, the sum of S over all permutations is congruent to the sum of all residues modulo n!, i.e. `n! line 59 source
Source documentation
Assuming the opposite of what is to be proved, the sum of S over all permutations is congruent to the sum of all residues modulo n!, i.e. n! * (n! - 1) / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Not, Exists, Equiv.Perm, And, Ne, Dvd.dvd, Nat.factorial, HSub.hSub, Imo2001Q4.S, Int.ModEq, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Finset.sum, Finset.univ
Proof uses: Membership.mem, Finset, Finset.Ico, HMod.hMod, Eq.mpr, LE.le, LT.lt, id, Eq, congrArg, propext, Finset.mem_Ico, And.intro, Int.emod_nonneg, ne_of_gt, Iff.mpr, Nat.cast_pos', Nat.factorial_pos, Int.emod_lt_of_pos, Subtype and 57 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma sum_range_modEq_sum_of_contra (hS : ¬∃ a b, a ≠ b ∧ (n ! : ℤ) ∣ S c a - S c b) :
    n ! * ((n ! : ℤ) - 1) / 2 ≡ ∑ a, S c a [ZMOD n !] := by
…
```
Mentions: Imo2001Q4.S
lemma Imo2001Q4.sum_perm_add_one The sum over all permutations of Icc 1 n of the entry at any fixed position is `(n - 1)! line 87 source
Source documentation
The sum over all permutations of Icc 1 n of the entry at any fixed position is (n - 1)! * (n * (n + 1) / 2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, LE.le, OfNat.ofNat, Eq, Finset.sum, Equiv.Perm, Finset.univ, HAdd.hAdd, HMul.hMul, Nat.factorial, HSub.hSub, HDiv.hDiv
Proof uses: Exists, Eq.mp, congrArg, propext, le_iff_exists_add', Eq.mpr, Equiv, Equiv.mulRight, Equiv.swap, id, Eq.symm, Equiv.sum_comp, Function.comp, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, add_tsub_cancel_right, Equiv.swap_apply_left and 29 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma sum_perm_add_one {i : Fin n} (hn : 1 ≤ n) :
    ∑ a : Perm (Fin n), ((a i).1 + 1) = (n - 1)! * (n * (n + 1) / 2) := by
…
```
lemma Imo2001Q4.sum_modEq_zero_of_odd For odd n, the sum of S over all permutations is divisible by n! line 101 source
Source documentation
For odd n, the sum of S over all permutations is divisible by n!.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Odd, Int.ModEq, Nat.factorial, Finset.sum, Equiv.Perm, Finset.univ, Imo2001Q4.S, OfNat.ofNat
Proof uses: id, Eq.mpr, HMul.hMul, HAdd.hAdd, Eq, congrArg, Finset.sum_comm, Eq.rec, Eq.refl, funext, Eq.trans, Eq.symm, Nat.cast_one, Nat.cast_add, congrFun', Finset.sum_congr, Finset, Membership.mem, HSub.hSub, HDiv.hDiv and 16 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma sum_modEq_zero_of_odd (hn : Odd n) : ∑ a, S c a ≡ 0 [ZMOD n !] := by
…
```
Mentions: Imo2001Q4.S
problem Imo2001Q4.imo2001_p4 line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, And, Odd, LT.lt, OfNat.ofNat, Exists, Equiv.Perm, Ne, Dvd.dvd, Nat.factorial, HSub.hSub, Imo2001Q4.S
Proof uses: Decidable.byContradiction, Eq, Not, Int.ModEq, HDiv.hDiv, HMul.hMul, Int.ModEq.trans, Finset.sum, Finset.univ, Imo2001Q4.sum_range_modEq_sum_of_contra, Imo2001Q4.sum_modEq_zero_of_odd, And.left, False, Eq.mp, congrArg, propext, dvd_def, Int.modEq_zero_iff_dvd, cast, Eq.symm and 20 more
95 instances, coercions and auxiliary constants left out.

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