`Compfiles/Usa1982P2.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 1982, Problem 2

Show that if m, n are positive integers such that (x^(m+n) + y^(m+n) + z^(m+n))/(m+n) = ((x^m + y^m + z^m)/m) ((x^n + y^n + z^n)/n) for all real x, y, z with sum 0, then {m, n} = {2, 3} or {2, 5}.

Imports (16)

Imported by 1 file

Compfiles.lean

def Usa1982P2.auxPoly The polynomial 1 + X^k + (-1 - X)^k over ℝ line 47 source
Source documentation
The polynomial 1 + X^k + (-1 - X)^k over ℝ. It arises from substituting x = 1, y = t, z = -1 - t into x^k + y^k + z^k (note 1 + t + (-1 - t) = 0).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Polynomial, Real
Proof uses: HAdd.hAdd, OfNat.ofNat, HPow.hPow, Polynomial.X, HSub.hSub, RingHom, Polynomial.C, Neg.neg
19 instances, coercions and auxiliary constants left out.
```
noncomputable def auxPoly (k : ℕ) : ℝ[X] := 1 + X ^ k + (C (-1) - X) ^ k
```
lemma Usa1982P2.auxPoly_eval line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Polynomial.eval, Usa1982P2.auxPoly, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HSub.hSub, Neg.neg
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Polynomial, Polynomial.X, RingHom, Polynomial.C, map_neg, map_one, Polynomial.eval_add, congr, Polynomial.eval_one, Polynomial.eval_pow, Polynomial.eval_X, Polynomial.eval_sub, Polynomial.eval_neg, eq_self
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Usa1982P2.auxPoly_one line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Polynomial, Real, Usa1982P2.auxPoly, OfNat.ofNat, Nat
Proof uses: RingHom, Polynomial.C, Neg.neg, of_eq_true, Eq.trans, True, congrFun', congrArg, map_neg, map_one, eq_self, id, Eq.mpr, HAdd.hAdd, HPow.hPow, Polynomial.X, HSub.hSub, pow_one, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 34 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Usa1982P2.auxPoly_eq Rewrite (-1 - X)^k as (-1)^k (1 + X)^k line 60 source
Source documentation
Rewrite (-1 - X)^k as (-1)^k (1 + X)^k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Polynomial, Real, Usa1982P2.auxPoly, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Polynomial.X, HMul.hMul, RingHom, Polynomial.C, Neg.neg
Proof uses: HSub.hSub, of_eq_true, Eq.trans, True, congrFun', congrArg, map_neg, map_one, eq_self, Eq.mpr, id, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 21 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma auxPoly_eq (k : ℕ) :
    auxPoly k = 1 + X ^ k + C ((-1 : ℝ) ^ k) * (1 + X) ^ k := by
…
```
Mentions: Usa1982P2.auxPoly
lemma Usa1982P2.auxPoly_coeff_self line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Real, Finsupp, Polynomial.coeff, Usa1982P2.auxPoly, HAdd.hAdd, HPow.hPow, Neg.neg
Proof uses: Eq.mpr, Polynomial, Polynomial.X, HMul.hMul, RingHom, Polynomial.C, id, congrArg, Usa1982P2.auxPoly_eq, Polynomial.coeff_add, ite, Polynomial.coeff_one, Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Nat.choose, Polynomial.coeff_one_add_X_pow, Ne, of_eq_true, Eq.trans, True and 10 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Usa1982P2.auxPoly_coeff_pred line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, Real, Finsupp, Polynomial.coeff, Usa1982P2.auxPoly, HSub.hSub, HMul.hMul, HPow.hPow, Neg.neg
Proof uses: Eq.mpr, HAdd.hAdd, Polynomial, Polynomial.X, RingHom, Polynomial.C, id, congrArg, Usa1982P2.auxPoly_eq, Polynomial.coeff_add, ite, Polynomial.coeff_one, Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Nat.choose, Polynomial.coeff_one_add_X_pow, Ne, Nat.choose_symm, Nat.choose_one_right, Eq.refl and 10 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Usa1982P2.natDegree_auxPoly_le line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Polynomial.natDegree, Real, Usa1982P2.auxPoly
Proof uses: HSub.hSub, Polynomial, RingHom, Polynomial.C, Neg.neg, OfNat.ofNat, Polynomial.X, le_trans, Max.max, Polynomial.natDegree_sub_le, Eq.mpr, id, Eq, congrArg, Polynomial.natDegree_C, Polynomial.natDegree_X, max_le, Nat.zero_le, le_refl, HPow.hPow and 11 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma Usa1982P2.auxPoly_mul_eq The polynomial identity obtained from the functional equation by substituting x = 1, y = t, z = -1 - t and clearing denominators line 106 source
Source documentation
The polynomial identity obtained from the functional equation by substituting x = 1, y = t, z = -1 - t and clearing denominators.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Eq, HAdd.hAdd, HDiv.hDiv, HPow.hPow, HMul.hMul, Polynomial, Usa1982P2.auxPoly, RingHom, Polynomial.C
Proof uses: Ne, cast, Not, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, LT.lt.ne', ne_of_gt, add_pos', Iff.mpr, Nat.cast_pos', Polynomial.funext, HSub.hSub, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance and 94 more
149 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma auxPoly_mul_eq (m n : ℕ) (hm : 0 < m) (hn : 0 < n)
    (h : ∀ x y z : ℝ, x + y + z = 0 →
      (x ^ (m + n) + y ^ (m + n) + z ^ (m + n)) / (m + n) =
        (x ^ m + y ^ m + z ^ m) / m * ((x ^ n + y ^ n + z ^ n) / n)) :
    auxPoly (m + n) * C ((m : ℝ) * n) = auxPoly m * auxPoly n * C ((m : ℝ) + n) := by
…
```
Mentions: h, Usa1982P2.auxPoly
lemma Usa1982P2.coeff_eq Comparison of the coefficients of X ^ (m + n - 1) in auxPoly_mul_eq line 123 source
Source documentation
Comparison of the coefficients of X ^ (m + n - 1) in auxPoly_mul_eq.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Polynomial, Real, HMul.hMul, Usa1982P2.auxPoly, HAdd.hAdd, RingHom, Polynomial.C, HPow.hPow, Neg.neg, Finsupp, Polynomial.coeff, HSub.hSub
Proof uses: Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, Prod.fst, Prod.snd, LE.le, Finset, Insert.insert, Prod.mk, Singleton.singleton, Eq.mpr, And, Membership.mem, id, congrArg, propext, Finset.insert_subset_iff, Finset.singleton_subset_iff, And.intro, Finset.HasAntidiagonal.mem_antidiagonal and 77 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma coeff_eq (m n : ℕ) (hm : 0 < m) (hn : 0 < n)
    (hid : auxPoly (m + n) * C ((m : ℝ) * n) = auxPoly m * auxPoly n * C ((m : ℝ) + n)) :
    (-1 : ℝ) ^ (m + n) * ((m : ℝ) + n) * ((m : ℝ) * n) =
      ((auxPoly m).coeff (m - 1) * (auxPoly n).coeff n +
        (auxPoly m).coeff m * (auxPoly n).coeff (n - 1)) * ((m : ℝ) + n) := by
…
```
Mentions: Usa1982P2.auxPoly
lemma Usa1982P2.final_odd With n = 2 and m odd, evaluating the equation at (x, y, z) = (1, 1, -2) forces m ∈ {3, 5} line 171 source
Source documentation
With n = 2 and m odd, evaluating the equation at (x, y, z) = (1, 1, -2) forces m ∈ {3, 5}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Odd, Real, HAdd.hAdd, HDiv.hDiv, HPow.hPow, HMul.hMul, Or
Proof uses: Odd.add_even, Exists.intro, rfl, Neg.neg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_add, Int.ofNat, Int.negOfNat, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isInt, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isInt_neg, Mathlib.Meta.NormNum.instAtLeastTwo, Int, Nat.cast_zero, Ne and 150 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma final_odd (m n : ℕ) (hm : 0 < m) (hn : n = 2) (hmo : Odd m)
    (h : ∀ x y z : ℝ, x + y + z = 0 →
      (x ^ (m + n) + y ^ (m + n) + z ^ (m + n)) / (m + n) =
        (x ^ m + y ^ m + z ^ m) / m * ((x ^ n + y ^ n + z ^ n) / n)) :
    m = 3 ∨ m = 5 := by
…
```
Mentions: h
problem Usa1982P2.usa1982_p2 line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Eq, HAdd.hAdd, HDiv.hDiv, HPow.hPow, HMul.hMul, Or, And
Proof uses: Ne, cast, Not, Eq.symm, Eq.trans, congrArg, Nat.cast_zero, LT.lt.ne', ne_of_gt, add_pos', Iff.mpr, Nat.cast_pos', Neg.neg, Finsupp, Polynomial.coeff, Usa1982P2.auxPoly, HSub.hSub, Usa1982P2.coeff_eq, Usa1982P2.auxPoly_mul_eq, Mathlib.Meta.NormNum.isNat_eq_true and 173 more
218 instances, coercions and auxiliary constants left out.

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