Compfiles/Usa2011P4.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2011, Problem 4

For any integer n ≥ 2, define P(n) to be the proposition:

P(n) ≡ 2^(2^n) % (2^n - 1) is a power of 4

Either prove that P(n) is always true, or find a counterexample.

Imports (2)
Imported by 1 file
  1. abbrev Usa2011P4.P line 29 source

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: Exists, Eq, HPow.hPow, OfNat.ofNat, HMod.hMod, HSub.hSub

    9 instances, coercions and auxiliary constants left out.

  2. inductive Usa2011P4.SolutionData line 31 source

    no axioms what this means

  3. determine Usa2011P4.solution_data line 35 source

    no axioms what this means

    Statement uses: Usa2011P4.SolutionData

    Proof uses: Usa2011P4.SolutionData.Counterexample, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

  4. problem Usa2011P4.usa2011_p4 line 37 source

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

    Statement uses: Usa2011P4.usa2011_p4.match_1, Usa2011P4.SolutionData, Usa2011P4.solution_data, Unit, Nat, LE.le, OfNat.ofNat, Usa2011P4.P, And, Not

    Proof uses: id, And.intro, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Eq.mpr, Eq, HPow.hPow, HMod.hMod, HSub.hSub, congrArg, Exists, propext, not_exists, HMul.hMul, Nat.pow_right_injective, Eq.mp, Mathlib.Meta.NormNum.isNat_eq_true and 23 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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