imo-v1 / imo2021p5

imo2021p5

open

difficulty 4

credited

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

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

import Mathlib

abbrev Position : Type := Fin 2021 ≃ Fin 2021
def Position.swapped (p : Position) (k : Fin 2021) : Fin 2021 × Fin 2021 :=
  (p ((p.symm k) - 1), p ((p.symm k) + 1))
def move (p : Position × Fin 2021) : Position × Fin 2021 :=
  (p.1.trans (Equiv.swap (p.1.swapped p.2).1 (p.1.swapped p.2).2), p.2 + 1)
def Position.nth (p : Position) (n : Fin 2021) : Position := (move^[n] (p, 0)).1

theorem imo2021p5 (p : Position) :
    ∃ k, (((p.nth k).swapped k).1 < k ∧ k < ((p.nth k).swapped k).2) ∨
      (((p.nth k).swapped k).2 < k ∧ k < ((p.nth k).swapped k).1) := by
  sorry

Runs (0)

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