imo-v1 / imo2023p3

imo2023p3

open

difficulty 4

credited

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

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/imo2023p3.lean

import Mathlib

open scoped Polynomial
def answer : Set.Ici 2 → Set (ℕ → ℕ) := sorry

theorem imo2023p3 : (fun (k : Set.Ici 2) ↦ {a : ℕ → ℕ |
    (∀ i, 0 < a i) ∧ ∃ P : ℕ[X], P.Monic ∧ P.degree = k ∧
    ∀ n, P.eval (a n) = ∏ i ∈ Finset.Icc (n + 1) (n + ↑k), a i}) = answer := by
  sorry

Runs (0)

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