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

9 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2005, Problem 6

In a mathematical competition 6 problems were posed to the contestants. Each pair of problems was solved by more than 2/5 of the contestants. Nobody solved all 6 problems. Show that there were at least 2 contestants who each solved exactly 5 problems.

Imports (9)

Imported by 1 file

Compfiles.lean

theorem Imo2005P6.arith_core The arithmetic heart of the problem: fifteen pair counts, each at least (2 * n + 1) / 5, with sum 6 * n + 4 and satisfying ten congruences modulo 3, cannot exist line 47 source
Source documentation
The arithmetic heart of the problem: fifteen pair counts, each at least (2 * n + 1) / 5, with sum 6 * n + 4 and satisfying ten congruences modulo 3, cannot exist. The congruence for the pair {a, b} ⊆ {0, 1, 2, 3, 4} involves the counts for the pairs contained in the complementary triple together with the pairs joining the triple to problem 5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, LE.le, Int.ModEq, Int, False
Proof uses: HDiv.hDiv, HMod.hMod, Nat.div_add_mod, rfl, Or, Eq.mp, congrArg, And, Decidable.byContradiction, Not, dite, Exists, propext, Int.modEq_iff_add_fac, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 62 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 231 steps (first 200 of 231)
Open to load the checked before-and-after goal states.
```
theorem arith_core (n : ℕ)
    (t01 t02 t03 t04 t05 t12 t13 t14 t15 t23 t24 t25 t34 t35 t45 : ℕ)
    (hsum : t01 + t02 + t03 + t04 + t05 + t12 + t13 + t14 + t15 + t23 + t24 + t25 + t34 + t35 + t45
      = 6 * n + 4)
    (h01 : 2 * n + 1 ≤ 5 * t01) (h02 : 2 * n + 1 ≤ 5 * t02) (h03 : 2 * n + 1 ≤ 5 * t03)
    (h04 : 2 * n + 1 ≤ 5 * t04) (h05 : 2 * n + 1 ≤ 5 * t05) (h12 : 2 * n + 1 ≤ 5 * t12)
    (h13 : 2 * n + 1 ≤ 5 * t13) (h14 : 2 * n + 1 ≤ 5 * t14) (h15 : 2 * n + 1 ≤ 5 * t15)
    (h23 : 2 * n + 1 ≤ 5 * t23) (h24 : 2 * n + 1 ≤ 5 * t24) (h25 : 2 * n + 1 ≤ 5 * t25)
    (h34 : 2 * n + 1 ≤ 5 * t34) (h35 : 2 * n + 1 ≤ 5 * t35) (h45 : 2 * n + 1 ≤ 5 * t45)
    (c01 : (t01 : ℤ) ≡ 1 + t25 + t35 + t45 + t23 + t24 + t34 [ZMOD 3])
    (c02 : (t02 : ℤ) ≡ 1 + t15 + t35 + t45 + t13 + t14 + t34 [ZMOD 3])
    (c03 : (t03 : ℤ) ≡ 1 + t15 + t25 + t45 + t12 + t14 + t24 [ZMOD 3])
…
```
theorem Imo2005P6.cong_aux Documented declaration: cong_aux line 237 source
Source documentation
For every 2-subset P of the five problems {0, 1, 2, 3, 4} and every 4-subset st of all six problems, the per-contestant contribution to the mod-3 congruences (the indicator of solving P, minus the indicators of solving {u, 5} for u in the complementary triple, minus the indicators of solving the pairs inside the triple) is divisible by 3. This finite check is the content of Evan Chen's second claim.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, LE.le, Finset.erase, Finset.univ, Eq, Finset.card, Int.ModEq, Int, HSub.hSub, ite, Finset.sum, SDiff.sdiff, Insert.insert, Singleton.singleton, Finset.powersetCard
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem cong_aux : ∀ (P st : Finset (Fin 6)), P ⊆ Finset.univ.erase 5 → P.card = 2 →
    st.card = 4 →
    ((if P ⊆ st then (1 : ℤ) else 0)
      - ∑ u ∈ Finset.univ.erase 5 \ P, (if ({u, 5} : Finset (Fin 6)) ⊆ st then (1 : ℤ) else 0)
      - ∑ Q ∈ (Finset.univ.erase 5 \ P).powersetCard 2,
          (if Q ⊆ st then (1 : ℤ) else 0)) ≡ 0 [ZMOD 3] := by
…
```
Mentions: P
theorem Imo2005P6.pc2_univ The fifteen 2-subsets of Fin 6, as a literal finset line 246 source
Source documentation
The fifteen 2-subsets of Fin 6, as a literal finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Finset, Fin, OfNat.ofNat, Nat, Finset.powersetCard, Finset.univ, Insert.insert, Singleton.singleton
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem pc2_univ : (Finset.univ : Finset (Fin 6)).powersetCard 2 =
    {{0, 1}, {0, 2}, {0, 3}, {0, 4}, {0, 5}, {1, 2}, {1, 3}, {1, 4}, {1, 5}, {2, 3}, {2, 4},
      {2, 5}, {3, 4}, {3, 5}, {4, 5}} := by
…
```
theorem Imo2005P6.exists_superset_card Any set of at most k ≤ 6 problems can be extended to a set of exactly k problems line 252 source
Source documentation
Any set of at most k ≤ 6 problems can be extended to a set of exactly k problems.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Fin, OfNat.ofNat, Nat, LE.le, Finset.card, Exists, And, Eq
Proof uses: Compl.compl, HSub.hSub, Finset.exists_subset_card_eq, Eq.mpr, Fintype.card, id, congrArg, Finset.card_compl, Fintype.card_fin, Exists.intro, Union.union, And.intro, Finset.subset_union_left, HAdd.hAdd, Finset.card_union_of_disjoint, Iff.mp, Disjoint, Finset.subset_compl_iff_disjoint_left
24 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem exists_superset_card {s : Finset (Fin 6)} {k : ℕ} (h1 : s.card ≤ k) (h2 : k ≤ 6) :
    ∃ t : Finset (Fin 6), s ⊆ t ∧ t.card = k := by
…
```
def Imo2005P6.pairCount The number of contestants who solved both problems of the pair P line 263 source
Source documentation
The number of contestants who solved both problems of the pair P.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, OfNat.ofNat
Proof uses: Finset.card, Finset.filter, LE.le, Finset.univ
8 instances, coercions and auxiliary constants left out.
```
def pairCount {n : ℕ} (s : Fin n → Finset (Fin 6)) (P : Finset (Fin 6)) : ℕ :=
…
```
Mentions: P
theorem Imo2005P6.pairCount_two line 266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, OfNat.ofNat, Eq, Imo2005P6.pairCount, Insert.insert, Singleton.singleton, Finset.card, Finset.filter, And, Membership.mem, Finset.univ
Proof uses: id, Eq.rec, Eq.refl, LE.le, Finset.ext, of_eq_true, Iff, Eq.trans, True, congr, congrArg, congrFun', Finset.filter_congr, Iff.of_eq, true_and, iff_self
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Imo2005P6.sum_pairCount Double counting: the sum of the pair counts over all fifteen pairs equals the sum over contestants of the number of pairs of problems they solved line 275 source
Source documentation
Double counting: the sum of the pair counts over all fifteen pairs equals the sum over contestants of the number of pairs of problems they solved.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, OfNat.ofNat, Eq, Finset.sum, Finset.powersetCard, Finset.univ, Imo2005P6.pairCount, Finset.card
Proof uses: Finset.bipartiteBelow, LE.le, Finset.ext, Eq.mpr, Iff, Membership.mem, And, id, congr, congrArg, Eq.trans, congrFun', Iff.intro, And.intro, Finset.subset_univ, Trans.trans, Finset.bipartiteAbove, Finset.sum_congr, rfl, Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow and 1 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem sum_pairCount {n : ℕ} (s : Fin n → Finset (Fin 6)) :
    ∑ P ∈ (Finset.univ : Finset (Fin 6)).powersetCard 2, pairCount s P
      = ∑ i, ((s i).powersetCard 2).card := by
…
```
Mentions: P, Imo2005P6.pairCount
theorem Imo2005P6.pairCount_modEq Documented declaration: pairCount_modEq line 304 source
Source documentation
The congruences: for every pair P ⊆ {0, 1, 2, 3, 4} of problems, writing T for the complementary triple, the number of contestants solving P is congruent modulo 3 to 1 + ∑_{u ∈ T} (contestants solving {u, 5}) + ∑_{Q ∈ T choose 2} (contestants solving Q). This holds per contestant: the distinguished contestant c0 (who solved exactly {0, 1, 2, 3, 4}) contributes -2 ≡ 1, and every other contestant, who solved exactly four problems, contributes a multiple of 3 (see cong_aux).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, OfNat.ofNat, Eq, Finset.erase, Finset.univ, Ne, Finset.card, Membership.mem, Finset.powersetCard, Int.ModEq, Int, Imo2005P6.pairCount, HAdd.hAdd, Finset.sum, SDiff.sdiff, Insert.insert, Singleton.singleton
Proof uses: LE.le, And, Iff.mp, Finset.mem_powersetCard, Eq.mpr, id, congrArg, rfl, ite, Finset.natCast_card_filter, Finset.sum_congr, Finset.sum_comm, Eq.refl, HSub.hSub, Iff.mpr, Dvd.dvd, Int.modEq_zero_iff_dvd, Finset.dvd_sum, Imo2005P6.cong_aux, And.left and 108 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 49 steps
Open to load the checked before-and-after goal states.
```
theorem pairCount_modEq {n : ℕ} {s : Fin n → Finset (Fin 6)} {c0 : Fin n}
    (hc0 : s c0 = Finset.univ.erase 5) (h4 : ∀ i : Fin n, i ≠ c0 → (s i).card = 4)
    {P : Finset (Fin 6)} (hP : P ∈ (Finset.univ.erase 5 : Finset (Fin 6)).powersetCard 2) :
    (pairCount s P : ℤ)
      ≡ 1 + ∑ u ∈ Finset.univ.erase 5 \ P, (pairCount s {u, 5} : ℤ)
        + ∑ Q ∈ (Finset.univ.erase 5 \ P).powersetCard 2, (pairCount s Q : ℤ) [ZMOD 3] := by
…
```
Mentions: P, Imo2005P6.pairCount
problem Imo2005P6.imo2005_p6 line 373 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Finset, OfNat.ofNat, Ne, LT.lt, HMul.hMul, Finset.card, Finset.filter, And, Membership.mem, Finset.univ, Exists, Eq
Proof uses: Decidable.byContradiction, Not, False, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Nat.lt_irrefl, Eq.mp, congrArg, MulZeroClass.mul_zero, EmptyCollection.emptyCollection, Finset.card_empty, Finset.filter_empty, Finset.univ_eq_empty, Eq.symm, Eq.trans, binderNameHint and 148 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 332 steps (first 200 of 332)
Open to load the checked before-and-after goal states.