Compfiles/Imo1982P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1982, Problem 4

Prove that if n is a positive integer such that the equation

x3 - 3xy^2 + y^3 = n

has a solution in integers x, y, then it has at least three such solutions. Show that the equation has no solutions in integers for n = 2891.

Imports (2)
Imported by 1 file
  1. lemma Imo1982P4.lemma1 line 32 source

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

    Statement uses: ZMod, OfNat.ofNat, Nat, Eq, HAdd.hAdd, HSub.hSub, HPow.hPow, HMul.hMul, And

    Proof uses: List, List.Mem, Fin, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, Eq.mpr, id, and_self, Eq.refl, eq_of_heq and 10 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  2. problem Imo1982P4.imo1982_p4 line 39 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Int, Eq, HAdd.hAdd, HSub.hSub, HPow.hPow, HMul.hMul, And, Ne, Or

    Proof uses: False, HMod.hMod, Int.ModEq, Eq.mpr, Dvd.dvd, id, Eq.trans, congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.isInt_emod, Int.ofNat, Mathlib.Meta.NormNum.IsNat.to_isInt, Bool, Bool.true, ZMod and 108 more

    144 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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