Compfiles/Imo2003P2.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2003, Problem 2

Determine all pairs of positive integers (a,b) such that

a²/(2ab² - b³ + 1)

is a positive integer.

Imports (2)
Imported by 1 file
  1. lemma Imo2003P2.aux₁ line 31 source

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

    Statement uses: Int, LT.lt, OfNat.ofNat, HMul.hMul, HPow.hPow, Nat

    Proof uses: LE.le, one_le_pow₀

    26 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. determine Imo2003P2.solution_set line 37 source

    standard axioms: propext what this means

    Statement uses: Set, Prod, Int

    Proof uses: Union.union, Set.ofPred, Imo2003P2.solution_set.match_1, Exists, And, LT.lt, OfNat.ofNat, Eq, HMul.hMul, HSub.hSub, HPow.hPow, Nat

    12 instances, coercions and auxiliary constants left out.

  3. problem Imo2003P2.imo2003_p2 line 41 source

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

    Statement uses: Int, Iff, Membership.mem, Prod, Set, Imo2003P2.solution_set, Prod.mk, And, LT.lt, OfNat.ofNat, Exists, Eq, HMul.hMul, HAdd.hAdd, HSub.hSub, HPow.hPow, Nat

    Proof uses: Iff.intro, Union.union, Set.ofPred, Imo2003P2.solution_set.match_1, Eq.mpr, id, congrArg, And.intro, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Mathlib.Meta.NormNum.isNat_lt_true, Bool.false, Exists.intro, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr and 133 more

    154 instances, coercions and auxiliary constants left out.

    Tactic trace: 168 steps

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