`Compfiles/Imo2011P1.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 2011, Problem 1

Given any set A = {a₁, a₂, a₃, a₄} of four distinct positive integers, we denote the sum a₁ + a₂ + a₃ + a₄ by s_A. Let n_A denote the number of pairs (i, j) with 1 ≤ i < j ≤ 4 for which a_i + a_j divides s_A. Find all sets A of four distinct positive integers which achieve the largest possible value of n_A.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2011P1.pairCount The number of two-element subsets of A whose sum divides the sum of A line 30 source
Source documentation
The number of two-element subsets of A whose sum divides the sum of A.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Finset.card, Finset.filter, Dvd.dvd, Finset.sum, Finset.powersetCard, OfNat.ofNat
4 instances, coercions and auxiliary constants left out.
```
def pairCount (A : Finset ℕ) : ℕ :=
…
```
determine Imo2011P1.SolutionSet line 33 source
standard axioms: Quot.sound, propext what this means
Statement uses: Set, Finset, Nat
Proof uses: Set.ofPred, Exists, And, LT.lt, OfNat.ofNat, Or, Eq, Insert.insert, HMul.hMul, Singleton.singleton
7 instances, coercions and auxiliary constants left out.
lemma Imo2011P1.mem_pair line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Insert.insert, Singleton.singleton, Or, Eq
Proof uses: Eq.mp, Eq.trans, congrArg
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P1.pair_ne_pair line 42 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Or, And, Ne, Finset, Insert.insert, Singleton.singleton
Proof uses: Eq, False, Membership.mem, Eq.mpr, id, congrArg, Eq.symm, of_eq_true, Eq.trans, True, congr, eq_self, true_or, Imo2011P1.mem_pair, rfl, or_true
13 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P1.not_dvd_between A natural number strictly between m and 2 * m is not divisible by m line 56 source
Source documentation
A natural number strictly between m and 2 * m is not divisible by m.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, HMul.hMul, OfNat.ofNat, Not, Dvd.dvd
Proof uses: absurd, Eq, False, Nat.eq_of_dvd_of_lt_two_mul
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma not_dvd_between {m s : ℕ} (h1 : m < s) (h2 : s < 2 * m) : ¬ m ∣ s := fun h ↦
…
```
Mentions: h
lemma Imo2011P1.pair_mem_powersetCard_two line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Membership.mem, Ne, Finset.powersetCard, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: Iff.mpr, And, LE.le, Eq, Finset.card, Finset.mem_powersetCard, And.intro, Finset.insert_subset, Finset.singleton_subset_iff, Finset.card_pair
15 instances, coercions and auxiliary constants left out.
lemma Imo2011P1.sum_four line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, Finset.sum, Insert.insert, Finset, Singleton.singleton, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Finset.sum_insert, Not, Membership.mem, Or, Eq.trans, Finset.sum_singleton, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 1 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P1.filter_subset_target The two-element subsets of {a, b, c, d} whose sum divides the total, viewed inside pairCount line 74 source
Source documentation
The two-element subsets of {a, b, c, d} whose sum divides the total, viewed inside pairCount.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Finset, Finset.filter, Dvd.dvd, Finset.sum, Insert.insert, Singleton.singleton, Finset.powersetCard, OfNat.ofNat, SDiff.sdiff
Proof uses: Eq, HAdd.hAdd, Imo2011P1.sum_four, Membership.mem, Eq.mpr, And, Not, id, congrArg, propext, Finset.mem_sdiff, And.intro, And.left, Eq.mp, Finset.mem_filter, And.right, Or, False, Finset.mem_singleton, Finset.mem_insert and 3 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma filter_subset_target {a b c d : ℕ} (hab : a < b) (hbc : b < c) (hcd : c < d) :
    ((({a, b, c, d} : Finset ℕ).powersetCard 2).filter
        fun p ↦ (∑ x ∈ p, x) ∣ ∑ x ∈ ({a, b, c, d} : Finset ℕ), x) ⊆
      ((({a, b, c, d} : Finset ℕ).powersetCard 2) \ {({b, d} : Finset ℕ), {c, d}}) := by
…
```
lemma Imo2011P1.card_target line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Eq, Finset.card, Finset, SDiff.sdiff, Finset.powersetCard, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: LE.le, Finset.insert_subset, Imo2011P1.pair_mem_powersetCard_two, of_eq_true, Membership.mem, Eq.trans, Or, True, congrArg, congr, eq_self, true_or, or_true, Iff.mpr, Finset.singleton_subset_iff, Eq.mpr, HSub.hSub, Inter.inter, id, Finset.card_sdiff and 18 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P1.pairCount_le_four line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, Imo2011P1.pairCount, Insert.insert, Finset, Singleton.singleton, OfNat.ofNat
Proof uses: Eq.mpr, Finset.card, Finset.filter, Dvd.dvd, Finset.sum, Finset.powersetCard, id, Eq, congrArg, Imo2011P1.pairCount.eq_1, SDiff.sdiff, Eq.symm, Imo2011P1.card_target, Finset.card_le_card, Imo2011P1.filter_subset_target
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2011P1.dvds_of_four_le If the count is (at least) 4, then all four candidate pairs divide the sum line 118 source
Source documentation
If the count is (at least) 4, then all four candidate pairs divide the sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, LE.le, OfNat.ofNat, Imo2011P1.pairCount, Insert.insert, Finset, Singleton.singleton, And, Dvd.dvd, HAdd.hAdd
Proof uses: Eq, Finset.sum, Imo2011P1.sum_four, Finset.filter, Finset.powersetCard, SDiff.sdiff, Finset.eq_of_subset_of_card_le, Imo2011P1.filter_subset_target, le_trans, Finset.card, Eq.mpr, id, congrArg, Imo2011P1.card_target, le_refl, Eq.mp, Imo2011P1.pairCount.eq_1, Membership.mem, Ne, Not and 23 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 42 steps
Open to load the checked before-and-after goal states.
```
lemma dvds_of_four_le {a b c d : ℕ} (hab : a < b) (hbc : b < c) (hcd : c < d)
    (h : 4 ≤ pairCount {a, b, c, d}) :
    (a + b ∣ a + b + c + d) ∧ (a + c ∣ a + b + c + d) ∧
    (a + d ∣ a + b + c + d) ∧ (b + c ∣ a + b + c + d) := by
…
```
Mentions: h, Imo2011P1.pairCount
lemma Imo2011P1.pairCount_eq_four If all four candidate pairs divide the sum, the count is exactly 4 line 150 source
Source documentation
If all four candidate pairs divide the sum, the count is exactly 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Dvd.dvd, HAdd.hAdd, Eq, Imo2011P1.pairCount, Insert.insert, Finset, Singleton.singleton, OfNat.ofNat
Proof uses: le_antisymm, Imo2011P1.pairCount_le_four, Finset.sum, Imo2011P1.sum_four, Eq.mpr, LE.le, Finset.card, Finset.filter, Finset.powersetCard, id, congrArg, Imo2011P1.pairCount.eq_1, Membership.mem, And, propext, Finset.mem_filter, And.intro, Imo2011P1.pair_mem_powersetCard_two, Finset.sum_pair, Or and 24 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 67 steps
Open to load the checked before-and-after goal states.
```
lemma pairCount_eq_four {a b c d : ℕ} (hab : a < b) (hbc : b < c) (hcd : c < d)
    (h1 : a + b ∣ a + b + c + d) (h2 : a + c ∣ a + b + c + d)
    (h3 : a + d ∣ a + b + c + d) (h4 : b + c ∣ a + b + c + d) :
    pairCount {a, b, c, d} = 4 := by
…
```
Mentions: Imo2011P1.pairCount
lemma Imo2011P1.classify The heart of the solution: if all four candidate pairs divide the sum, then the quadruple is (a, 5a, 7a, 11a) or (a, 11a, 19a, 29a) line 198 source
Source documentation
The heart of the solution: if all four candidate pairs divide the sum, then the quadruple is (a, 5a, 7a, 11a) or (a, 11a, 19a, 29a).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, Or, And, Eq, HMul.hMul
Proof uses: Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, 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_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Iff.mp, Nat.dvd_add_right, dvd_refl, Eq.mp, Nat.dvd_add_left and 28 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma classify {a b c d : ℕ} (ha : 0 < a) (hab : a < b) (hbc : b < c)
    (h1 : a + b ∣ a + b + c + d) (h2 : a + c ∣ a + b + c + d)
    (h3 : a + d ∣ a + b + c + d) (h4 : b + c ∣ a + b + c + d) :
    (b = 5 * a ∧ c = 7 * a ∧ d = 11 * a) ∨
    (b = 11 * a ∧ c = 19 * a ∧ d = 29 * a) := by
…
```
lemma Imo2011P1.exists_sorted_four Any 4-element finset of naturals can be listed in increasing order line 257 source
Source documentation
Any 4-element finset of naturals can be listed in increasing order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Finset.card, OfNat.ofNat, Exists, And, LT.lt, Insert.insert, Singleton.singleton
Proof uses: List, Finset.sort, LE.le, List.cons, List.nil, Iff.mp, List.length, List.length_eq_four, Eq.mpr, id, congrArg, Finset.length_sort, Eq.refl, List.Pairwise, List.SortedLT.pairwise, Finset.sortedLT_sort, List.toFinset, Finset.sort_toFinset, Exists.intro, And.intro and 17 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma exists_sorted_four {A : Finset ℕ} (hA : A.card = 4) :
    ∃ a b c d : ℕ, a < b ∧ b < c ∧ c < d ∧ A = {a, b, c, d} := by
…
```
problem Imo2011P1.imo2011_p1 line 273 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Eq, Finset.card, OfNat.ofNat, Membership.mem, LT.lt, Iff, Set, Imo2011P1.SolutionSet, LE.le, Imo2011P1.pairCount
Proof uses: Iff.intro, And, Or, Insert.insert, HMul.hMul, Singleton.singleton, Exists, Imo2011P1.exists_sorted_four, Imo2011P1.pairCount_eq_four, Exists.intro, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg and 37 more
50 instances, coercions and auxiliary constants left out.

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