imo-v1 / imo2025p3

imo2025p3

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal imo2025p3

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/imo2025p3.lean

import Mathlib

def Bonza (f : ℕ+ → ℕ+) : Prop := ∀ a b : ℕ+, (f a : ℤ) ∣ (b ^ (a : ℕ) : ℤ) - (f b ^ (f a : ℕ) : ℤ)
def answer : ℝ := sorry

theorem imo2025p3 : IsLeast {c : ℝ | ∀ f : ℕ+ → ℕ+, Bonza f → ∀ n, f n ≤ c * n}
    answer := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.