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

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1983, Problem 2

Prove that the zeros of

\[x^5+ax^4+bx^3+cx^2+dx+e=0\]

cannot all be real if $2a^2<5b$.

Imports (3)

Imported by 1 file

Compfiles.lean

lemma Usa1983P2.vieta follows https://artofproblemsolving.com/wiki/index.php/1983_USAMO_Problems/Problem_2 vieta formulas for a and b only, done very similarly to Usa2014P1.lean line 35 source
Source comment
follows https://artofproblemsolving.com/wiki/index.php/1983_USAMO_Problems/Problem_2 vieta formulas for a and b only, done very similarly to `Usa2014P1.lean`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fin, OfNat.ofNat, Nat, Eq, Polynomial, HMul.hMul, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, HAdd.hAdd, HPow.hPow, And, Neg.neg
Proof uses: And.intro, Mathlib.Tactic.LinearCombination.eq_of_eq, HDiv.hDiv, Polynomial.eval, Nat.iterate, LinearMap, RingHom.id, Polynomial.derivative, Mathlib.Tactic.LinearCombination.div_eq_const, Eq.symm, eq_of_heq, Semiring, HEq, Eq.refl, HEq.refl, Mathlib.Tactic.LinearCombination.eq_rearrange, Eq.mpr, id, congrFun', congrArg and 114 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma vieta {a b c d e : ℝ} {x : Fin 5 → ℝ}
  (hp: ((X - C (x 0)) * (X - C (x 1)) * (X - C (x 2)) * (X - C (x 3)) * (X - C (x 4))
    = X^5 + C a * X^4 + C b * X^3 + C c * X^2 + C d * X + C e)) :
    a = - ((x 0) + (x 1) + (x 2) + (x 3) + (x 4)) ∧
    b = (x 0)*(x 1) + (x 0)*(x 2) + (x 0)*(x 3) + (x 0)*(x 4)
      + (x 1)*(x 2) + (x 1)*(x 3) + (x 1)*(x 4)
      + (x 2)*(x 3) + (x 2)*(x 4) + (x 3)*(x 4)
      := by
…
```
theorem Usa1983P2.ineqs line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fin, OfNat.ofNat, Nat, Eq, Polynomial, HMul.hMul, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, HAdd.hAdd, HPow.hPow, LE.le, HDiv.hDiv
Proof uses: Neg.neg, And, Usa1983P2.vieta, Trans.trans, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_add and 108 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
problem Usa1983P2.usa1983_p2 line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fin, OfNat.ofNat, Nat, LT.lt, HMul.hMul, HPow.hPow, Not, Eq, Polynomial, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, HAdd.hAdd
Proof uses: Mathlib.Tactic.Contrapose.contrapose₃, Eq.mpr, LE.le, id, implies_congr, Eq.refl, HDiv.hDiv, Usa1983P2.ineqs, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, Ring and 71 more
116 instances, coercions and auxiliary constants left out.

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