Compfiles/Imo1982P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1982, Problem 1

Let f be a function from positive integers to nonnegative integers such that

  1. f(2) = 0
  2. f(3) > 0
  3. f(9999) = 3333
  4. for all m,n > 0, f (m + n) - f (m) - f(n) = 1 or 0

Determine the value of f(1982).

Imports (2)
Imported by 1 file
  1. determine Imo1982P1.solution_value line 31 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  2. problem Imo1982P1.imo1982_p1 line 33 source

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

    Statement uses: Nat, Eq, OfNat.ofNat, LT.lt, Or, HAdd.hAdd, Imo1982P1.solution_value

    Proof uses: Nat.one_pos, Eq.mp, congrArg, two_pos, congr, Eq.trans, add_zero, congrFun', zero_add, False.elim, False, of_eq_true, True, eq_self, LE.le, Nat.le_of_eq, Eq.symm, Nat.le.intro, HMul.hMul, Trans.trans and 46 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 85 steps

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