Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2025P3

module

public import Mathlib.Tactic
public import Mathlib.Data.ENat.Basic
public import Mathlib.NumberTheory.LSeries.PrimesInAP
public import Mathlib.NumberTheory.Multiplicity
public import Mathlib.Data.Nat.Basic
public import Mathlib.Data.Real.Basic
public import Mathlib.Order.Bounds.Basic

public section


/-!
# 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.
-/
open Int

def Bonza (f : ℕ+ → ℕ+) : Prop :=
  ∀ a b : ℕ+,
    (f a : Int) ∣ ((b : Int) ^ (a: ℕ) - (f b : Int) ^ ((f a): ℕ))

def is_valid_c (c : ℝ) : Prop :=
  ∀ (f : ℕ+ → ℕ+), Bonza f → ∀ n, (f n : ℝ) ≤ c * (n : ℝ)

/- determine -/ abbrev answer : ℝ := sorry

theorem imo2025_p3 :
  IsLeast {c: ℝ | is_valid_c c} answer := sorry

File author(s): Reuven Peleg (Problem statement) , Shahar Blumentzvaig

This problem has a complete formalized solution.