`Compfiles/Usa1997P5.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 1997, Problem 5

Let a, b, c be positive reals. Prove that 1 / (a³ + b³ + abc) + 1 / (b³ + c³ + abc) + 1 / (c³ + a³ + abc) ≤ 1 / abc

Imports (2)

Imported by 1 file

Compfiles.lean

lemma Usa1997P5.bound Bounding the individual fraction line 37 source
Source comment
Bounding the individual fraction

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul
Proof uses: Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, id, Eq, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Eq.trans, congr_arg₂, rfl, Mathlib.Tactic.FieldSimp.NF.div_eq_eval, Mathlib.Tactic.FieldSimp.NF.one_eq_eval and 105 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    1 / (a^3 + b^3 + a*b*c) ≤ 1 / (a^2*b + a*b^2 + a*b*c) := by
…
```
theorem Usa1997P5.main_sum Add the three bounds together line 44 source
Source comment
Add the three bounds together

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, HMul.hMul
Proof uses: Usa1997P5.bound, add_le_add
41 instances, coercions and auxiliary constants left out.
```
theorem main_sum (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    1 / (a ^ 3 + b ^ 3 + a * b * c) +
      (1 / (b ^ 3 + c ^ 3 + b * c * a) + 1 / (c ^ 3 + a ^ 3 + c * a * b)) ≤
    1 / (a ^ 2 * b + a * b ^ 2 + a * b * c) +
      (1 / (b ^ 2 * c + b * c ^ 2 + b * c * a) +
         1 / (c ^ 2 * a + c * a ^ 2 + c * a * b)):=
…
```
problem Usa1997P5.usa1997_p5 line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, HMul.hMul
Proof uses: Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, Inv.inv, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, id and 75 more
88 instances, coercions and auxiliary constants left out.

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