Compfiles/Imo1986P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1986, Problem 1

Let d be any positive integer not equal to 2, 5 or 13. Show that one can find distinct a, b in the set {2, 5, 13, d} such that ab - 1 is not a perfect square.

Imports (5)
Imported by 1 file
  1. theorem Imo1986P1.imo1986_p1' line 45 source

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

    Statement uses: Int, Not, And, IsSquare, HSub.hSub, HMul.hMul, OfNat.ofNat

    Proof uses: False, Eq, Odd, Iff.mp, HPow.hPow, Nat, Int.odd_pow', two_ne_zero, Exists.intro, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, Eq.mp, pow_two, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring and 99 more

    109 instances, coercions and auxiliary constants left out.

    Tactic trace: 71 steps

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

  2. problem Imo1986P1.imo1986_p1 line 102 source

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

    Statement uses: Int, LE.le, OfNat.ofNat, Ne, Exists, Subtype, Membership.mem, Finset, Insert.insert, Singleton.singleton, And, Not, Eq, HPow.hPow, Nat, HSub.hSub, HMul.hMul

    Proof uses: Classical.byContradiction, False, And.right, And.left, Eq.mp, Eq.trans, Or, congrArg, Subtype.mk, Iff.mpr, Iff.of_eq, funext, propext, exists_prop_congr, Eq.refl, congrFun', Subtype.mk.injEq, congr, forall_congr, implies_congr and 13 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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