Compfiles/Imo2025P3.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2025, Problem 3

Let N denote the set of positive integers.

A function f : N → N is said to be bonza if f(a) divides b ^ a − f(b) ^ f(a) for all positive integers a and b.

Determine the smallest real constant c such that f(n) ⩽ cn for all bonza functions f and all positive integers n.

Imports (8)
Imported by 1 file
  1. lemma fermat_little_theorem line 38 source

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

    Statement uses: PNat, Nat.Prime, Nat, Nat.ModEq, HPow.hPow

    Proof uses: dite, Dvd.dvd, OfNat.ofNat, Nat.ModEq.pow, Eq.mp, congrArg, Eq.symm, propext, Nat.modEq_zero_iff_dvd, Nat.ModEq.trans, zero_pow, of_eq_true, Not, Eq, Eq.trans, False, True, not_false_eq_true, Nat.ModEq.symm, Nat.Coprime and 14 more

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  2. lemma fermat_little_theorem2 line 55 source

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

    Statement uses: PNat, Nat.Prime, Nat, Nat.ModEq, HPow.hPow

    Proof uses: Nat.recAux, Eq.mpr, OfNat.ofNat, id, Eq, congrFun', congrArg, Eq.trans, pow_zero, pow_one, Eq.refl, HMod.hMod, HAdd.hAdd, HMul.hMul, Nat.pow_add, Nat.mul_comm, Nat.pow_mul, fermat_little_theorem, Nat.ModEq.pow, Nat.ModEq.trans

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  3. lemma int_dvd_to_nat_dvd line 68 source

    standard axioms: propext what this means

    Statement uses: PNat, Nat, Dvd.dvd, Int

    Proof uses: Iff.mp, Int.ofNat_dvd

    10 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. def Bonza line 74 source

    standard axioms: propext what this means

    Statement uses: PNat

    Proof uses: Dvd.dvd, Int, HSub.hSub, HPow.hPow, Nat

    10 instances, coercions and auxiliary constants left out.

  5. def is_valid_c line 78 source

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

    Statement uses: Real

    Proof uses: PNat, Bonza, LE.le, HMul.hMul

    6 instances, coercions and auxiliary constants left out.

  6. determine answer line 81 source

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

    Statement uses: Real

    Proof uses: OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  7. problem imo2025_p3 line 83 source

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

    Statement uses: IsLeast, Real, Set.ofPred, is_valid_c, answer

    Proof uses: id, OfNat.ofNat, And.intro, Membership.mem, Set, lowerBounds, PNat, Bonza, Dvd.dvd, Int, HPow.hPow, Nat, of_eq_true, Eq.trans, Or, Ne, IsUnit, True, congrFun', congrArg and 215 more

    276 instances, coercions and auxiliary constants left out.

    Tactic trace: 491 steps (first 200 of 491)

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