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

USA Mathematical Olympiad 2004, Problem 2

Suppose a₁, a₂, …, aₙ are integers whose greatest common divisor is 1. Let S be a set of integers with the following properties:

(a) For i = 1, 2, …, n, aᵢ ∈ S.

(b) For i, j = 1, 2, …, n (not necessarily distinct), aᵢ − aⱼ ∈ S.

Prove that S must equal the set of all integers.

Imports (8)

Imported by 1 file

Compfiles.lean

lemma Usa2004P2.bezout Bézout's identity for finitely many integers: the gcd of the values of a on a finset T is an integer linear combination of them line 50 source
Source documentation
Bézout's identity for finitely many integers: the gcd of the values of a on a finset T is an integer linear combination of them.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Finset, Exists, Eq, Finset.sum, HMul.hMul, Finset.gcd
Proof uses: Finset.induction_on, Exists.intro, EmptyCollection.emptyCollection, OfNat.ofNat, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum_congr, Eq.refl, Membership.mem, MulZeroClass.zero_mul, Finset.sum_const_zero, eq_self, Not, Insert.insert, Eq.mpr, GCDMonoid.gcd, id and 33 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma bezout (T : Finset (Fin n)) :
    ∃ c : Fin n → ℤ, ∑ i ∈ T, c i * a i = T.gcd a := by
…
```
lemma Usa2004P2.neg_mem From (b) with i = j we get 0 ∈ S, and then (c) with x = 0 shows that S is closed under negation line 74 source
Source documentation
From (b) with i = j we get 0 ∈ S, and then (c) with x = 0 shows that S is closed under negation.

standard axioms: propext what this means
Statement uses: Set, Int, Membership.mem, OfNat.ofNat, HAdd.hAdd, HSub.hSub, Neg.neg
Proof uses: Eq.mpr, id, Eq, congrArg, zero_add, Eq.mp, zero_sub
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma neg_mem (h0 : (0 : ℤ) ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    {s : ℤ} (hs : s ∈ S) : -s ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.add_mem_iff_sub_mem The key reformulation of condition (c): for x, y ∈ S, the membership of x + y and of x - y in S are equivalent line 82 source
Source documentation
The key reformulation of condition (c): for x, y ∈ S, the membership of x + y and of x - y in S are equivalent.

standard axioms: propext what this means
Statement uses: Set, Int, Membership.mem, OfNat.ofNat, HAdd.hAdd, HSub.hSub, Iff
Proof uses: Iff.intro, Neg.neg, Eq.mp, congrArg, sub_eq_add_neg, Usa2004P2.neg_mem, sub_neg_eq_add
28 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma add_mem_iff_sub_mem (h0 : (0 : ℤ) ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    {x y : ℤ} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S ↔ x - y ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.nat_mul_mem Any natural multiple of a generator lies in S line 91 source
Source documentation
Any natural multiple of a generator lies in S.

standard axioms: propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HAdd.hAdd, HSub.hSub, HMul.hMul
Proof uses: And, Nat.recAux, And.intro, Eq.mpr, id, Eq, congrArg, Eq.trans, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, zero_add, Nat.cast_one, one_mul, And.right, congr, Nat.cast_add, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 46 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma nat_mul_mem (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (k : Fin n) (c : ℕ) : (c : ℤ) * a k ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.sub_one_mem Any number of the form c * a i - a j with c : ℕ lies in S line 110 source
Source documentation
Any number of the form c * a i - a j with c : ℕ lies in S.

standard axioms: propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: And, Nat.recAux, And.intro, Eq.mpr, Neg.neg, id, Eq, congrArg, Eq.trans, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, zero_sub, Usa2004P2.neg_mem, zero_add, Nat.cast_one, one_mul, And.right, congr, Nat.cast_add and 48 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma sub_one_mem (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (i j : Fin n) (c : ℕ) : (c : ℤ) * a i - a j ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.nat_add_mem Any combination c * a i + d * a j with c d : ℕ lies in S line 131 source
Source documentation
Any combination c * a i + d * a j with c d : ℕ lies in S.

standard axioms: propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: And, Nat.recAux, And.intro, Eq.mpr, id, Eq, congrArg, Eq.trans, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, add_zero, Usa2004P2.nat_mul_mem, of_eq_true, True, zero_add, Nat.cast_one, one_mul, eq_self, Iff.mpr and 52 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma nat_add_mem (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (i j : Fin n) (c d : ℕ) : (c : ℤ) * a i + (d : ℤ) * a j ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.nat_sub_mem Any combination c * a i - d * a j with c d : ℕ lies in S line 158 source
Source documentation
Any combination c * a i - d * a j with c d : ℕ lies in S.

standard axioms: propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: And, Nat.recAux, And.intro, Eq.mpr, id, Eq, congrArg, Eq.trans, congrFun', CharP.cast_eq_zero, MulZeroClass.zero_mul, sub_zero, Usa2004P2.nat_mul_mem, of_eq_true, True, zero_add, Nat.cast_one, one_mul, eq_self, Usa2004P2.sub_one_mem and 52 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma nat_sub_mem (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (i j : Fin n) (c d : ℕ) : (c : ℤ) * a i - (d : ℤ) * a j ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.two_term_mem First lemma of the informal proof: any two-term integer linear combination c * a i + d * a j lies in S line 185 source
Source documentation
First lemma of the informal proof: any two-term integer linear combination c * a i + d * a j lies in S.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HMul.hMul
Proof uses: dite, LE.le, Eq, Exists, CanLift.prf, Usa2004P2.nat_add_mem, Not, Neg.neg, Exists.intro, Int.toNat, Eq.mpr, id, congrArg, Int.toNat_of_nonneg, Iff.mpr, neg_nonneg, LT.lt.le, Iff.mp, LT.lt, not_le and 46 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma two_term_mem (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (i j : Fin n) (c d : ℤ) : c * a i + d * a j ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.even_split Documented declaration: even_split line 214 source
Source documentation
Splitting step of the second lemma of the informal proof: if some coefficient c p is even, then ∑ i ∈ T, c i * a i can be written as x - y with x, y, x + y ∈ S, where membership of x and x + y comes from the induction hypothesis on strictly smaller finsets.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, Finset, LT.lt, Finset.sum, HMul.hMul, Ne, Even
Proof uses: Eq, Finset.erase, Iff.mpr, And, Finset.mem_erase, And.intro, Ne.symm, rfl, Function.update, Finset.erase_ssubset, Eq.mpr, id, congrArg, Eq.symm, Finset.add_sum_erase, Finset.ext, Iff, congr, Eq.trans, Iff.intro and 60 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma even_split (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    {T : Finset (Fin n)}
    (IH : ∀ U : Finset (Fin n), U ⊂ T → ∀ c : Fin n → ℤ, ∑ i ∈ U, c i * a i ∈ S)
    {c : Fin n → ℤ} {p q : Fin n} (hp : p ∈ T) (hq : q ∈ T) (hpq : p ≠ q)
    (hpe : Even (c p)) : ∑ i ∈ T, c i * a i ∈ S := by
…
```
Mentions: S
lemma Usa2004P2.all_linear_comb Second lemma of the informal proof: every integer linear combination of the generators lies in S line 268 source
Source documentation
Second lemma of the informal proof: every integer linear combination of the generators lies in S. Proved by strong induction on the finset T: vanishing coefficients are simply removed, an even coefficient allows the even_split step, and if all coefficients are odd one first perturbs two of them using u * a q = v * a p (where u = a p / gcd a p a q, v = a q / gcd a p a q) to manufacture an even coefficient.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Set, Membership.mem, OfNat.ofNat, HSub.hSub, HAdd.hAdd, Finset, Finset.sum, HMul.hMul
Proof uses: Finset.strongInduction, LT.lt, dite, Exists, And, Eq, Finset.erase, Eq.mpr, id, congrArg, Eq.symm, Finset.add_sum_erase, MulZeroClass.zero_mul, zero_add, Eq.refl, Finset.erase_ssubset, Not, LE.le, Finset.card, Or and 88 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 100 steps
Open to load the checked before-and-after goal states.
```
lemma all_linear_comb (h0 : (0 : ℤ) ∈ S) (ha : ∀ i, a i ∈ S)
    (hdiff : ∀ i j, a i - a j ∈ S)
    (hcond : ∀ x y : ℤ, x ∈ S → y ∈ S → x + y ∈ S → x - y ∈ S)
    (T : Finset (Fin n)) (c : Fin n → ℤ) : ∑ i ∈ T, c i * a i ∈ S := by
…
```
Mentions: S
problem Usa2004P2.usa2004_p2 line 357 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Set, Eq, Finset.gcd, Finset.univ, OfNat.ofNat, Membership.mem, HSub.hSub, HAdd.hAdd, Set.univ
Proof uses: Finset.sum, HMul.hMul, Exists, Usa2004P2.bezout, Finset, Finset.Nonempty, Decidable.byContradiction, Not, zero_ne_one, Eq.mp, EmptyCollection.emptyCollection, congrArg, Finset.gcd_empty, propext, Finset.not_nonempty_iff_eq_empty, sub_self, Usa2004P2.all_linear_comb, Eq.mpr, id, Finset.mul_sum and 21 more
76 instances, coercions and auxiliary constants left out.

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