imo-v1 / imo2021p6

imo2021p6

open

difficulty 4

credited

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

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

import Mathlib

open scoped Finset

theorem imo2021p6 {m : ℕ} (hm : 2 ≤ m) (A : Finset ℤ) (B : Fin m → Finset ℤ) (hBA : ∀ i, B i ⊆ A)
    (hB : ∀ k, ∑ i ∈ B k, i = m ^ ((k : ℕ) + 1)) : (m : ℚ) / 2 ≤ #A := by
  sorry

Runs (0)

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