Compfiles/Usa2001P1.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2001, Problem 1

Each of eight boxes contains six balls. Each ball has been colored with one of n colors, such that no two balls in the same box are the same color, and no two colors occur together in more than one box. Determine, with justification, the smallest integer n for which this is possible.

Imports (4)
Imported by 1 file
  1. def Usa2001P1.possible_num_colors line 31 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, Exists, Fin, OfNat.ofNat, Finset, And, Eq, Finset.card, Ne, Membership.mem, Not

    3 instances, coercions and auxiliary constants left out.

  2. determine Usa2001P1.min_colors line 38 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  3. lemma Usa2001P1.usa2001_p1_lemma if a₁, line 48 source

    Source documentation

    if a₁, ... a₆ is positive, ∑ (i=1 to 6), aᵢ ≤ 13 then ∑ (i=1 to 6) (1 / aᵢ) ≥ 36/13

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Finset, Eq, Nat, Finset.card, OfNat.ofNat, Membership.mem, GT.gt, LE.le, Finset.sum, Real, HDiv.hDiv

    Proof uses: Real.sqrt, HPow.hPow, HMul.hMul, Finset.sum_mul_sq_le_sq_mul_sq, Finset.sum_congr, rfl, of_eq_true, Eq.trans, inferInstance, CommGroupWithZero, True, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, List.nil, Prod, Int, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, congr_arg₂, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk and 81 more

    157 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

    Open to load the checked before-and-after goal states.

    lemma usa2001_p1_lemma {α} (s : Finset α) (sz : s.card = 6) (gen : α -> ℕ)
    (gt : ∀ i ∈ s, gen i > 0) (sum : (∑ i ∈ s, gen i) ≤ 13) :
    (36:ℝ)/(13:ℝ) ≤ (∑ i ∈ s, 1 / (gen i:ℝ)) := by
…
  4. problem Usa2001P1.usa2001_p1 line 79 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: IsLeast, Nat, Usa2001P1.possible_num_colors, Usa2001P1.min_colors

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Eq.mpr, Set.ofPred, Exists, Fin, OfNat.ofNat, Finset, And, Eq, Finset.card, Ne, Not, id, congrArg, Usa2001P1.possible_num_colors.eq_1, Unit, Insert.insert and 143 more

    140 instances, coercions and auxiliary constants left out.

    Tactic trace: 102 steps

    Open to load the checked before-and-after goal states.