imo-v1 / imo2020p5

imo2020p5

open

difficulty 4

credited

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

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

import Mathlib

open scoped Finset
def answer : Set ℕ := sorry

theorem imo2020p5 :
    {n : ℕ | 1 < n ∧ ∀ (deck : Fin n → ℕ), (∀ i, 0 < deck i) → (Pairwise fun j k ↦
      ∃ S : Finset (Fin n), S.Nonempty ∧
        (deck j + deck k : ℝ) / 2 = (∏ i ∈ S, (deck i : ℝ)) ^ (1 / (#S : ℝ))) →
      ∀ i j, deck i = deck j} = answer := by
  sorry

Runs (0)

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