IMO 2025 Problem 3: bonza functions
Follow the latest progress by email.
A function f:N→N on the positive integers is bonza if f(a) divides bᵃ−f(b)^(f(a)) for every positive a,b. Find the smallest real c such that f(n)≤cn for every bonza function and every positive integer n.
Why it matters and what counts as progress
Why it matters: It asks whether a nonlinear divisibility condition forces a sharp uniform linear growth bound.
What counts as progress: A sharp bound on f(n)/n for all bonza functions, with an extremal example establishing that the constant cannot decrease.
How the problem developed
- 15 Jul 2025 · Contest problem [1]
IMO jury The problem was set on this day of the official IMO 2025 contest.
Google DeepMind and Gemini Deep Think DeepMind reported an officially graded five-of-six result (35/42); its published solution collection includes a proof for this problem.
AI contributions 2
Aristotle formalizes five IMO 2025 solutions
Harmonic reports that Aristotle generated machine-verified solutions for 2025 IMO Problems 1–5 from human-formalized problem statements, with the Lean proofs published.
Gemini Deep Think solves five IMO 2025 problems
An advanced Gemini Deep Think model produced natural-language solutions to five of the six 2025 International Mathematical Olympiad problems, earning 35 of 42 points under the official coordinators’ grading.
Sources
Website timeline
Publication dates and editorial changes.