imo-v1 / imo2025p6

imo2025p6

open

difficulty 4

credited

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

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

import Mathlib

open scoped Finset Function
abbrev Cell : Type := Fin 2025 × Fin 2025
structure Tile where
  lowerLeft : Cell
  upperRight : Cell
  below_left : lowerLeft ≤ upperRight
def Tile.cells (t : Tile) : Set Cell := Set.Icc t.lowerLeft t.upperRight
def answer : ℕ := sorry

theorem imo2025p6 :
    IsLeast {k : ℕ | ∃ tiles : Fin k → Tile,
      Pairwise (Disjoint on (fun i ↦ (tiles i).cells)) ∧
      ∃ e : Fin 2025 ≃ Fin 2025, (⋃ i, (tiles i).cells)ᶜ = Set.range fun i ↦ (i, e i)} answer := by
  sorry

Runs (0)

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