AI-MO/CombiBench huggingface dataset:
Problem: There are $n\ge 2$ line segments in the plane such that every two segments cross and no three segments meet at a point. Geoff has to choose an endpoint of each segment and place a frog on it facing the other endpoint. Then he will clap his hands $n-1$ times. Every time he claps, each frog will immediately jump forward to the next intersection point on its segment. Frogs never change the direction of their jumps. Geoff wishes to place the frogs in such a way that no two of them will ever occupy the same intersection point at the same time. (a) Prove that Geoff can always fulfill his wish if $n$ is odd. (b) Prove that Geoff can never fulfill his wish if $n$ is even.

Lean formal statement:
import Mathlib

open Function

structure FrogSystem (N : ℕ) where
  
  otherSegment (s : Fin N) : Fin (N - 1) ≃ {s' : Fin N // s ≠ s'}
  
  point : {p : Sym2 (Fin N) // ¬ p.IsDiag} → EuclideanSpace ℝ (Fin 2)
  
  mem_collinear {s t₀ t₁ t₂} : t₀ < t₁ → t₁ < t₂ → Sbtw ℝ
      (point ⟨s(s, otherSegment s t₀), by simpa using (otherSegment s t₀).2⟩)
      (point ⟨s(s, otherSegment s t₁), by simpa using (otherSegment s t₁).2⟩)
      (point ⟨s(s, otherSegment s t₂), by simpa using (otherSegment s t₂).2⟩)

def FrogSystem.GeoffsWish {N : ℕ} (F : FrogSystem N) : Prop :=
  ∀ t, Injective fun s ↦ s(s, F.otherSegment s t)

theorem imo_2016_p6 :
    
    (∀ n ≥ 2, Odd n → ∃ F : FrogSystem n, F.GeoffsWish) ∧
    
      ∀ n ≥ 2, Even n → ∀ F : FrogSystem n, ¬ F.GeoffsWish := by sorry
Problem: A hunter and an invisible rabbit play a game in the Euclidean plane. The rabbit's starting point, $A_0$, and the hunter's starting point, $B_0$, are the same. After $n-1$ rounds of the game, the rabbit is at point $A_{n-1}$ and the hunter is at point $B_{n-1}$. In the nth round of the game, three things occur in order. (i) The rabbit moves invisibly to a point $A_n$ such that the distance between $A_{n-1}$ and $A_n$ is exactly 1. (ii) A tracking device reports a point $P_n$ to the hunter. The only guarantee provided by the tracking device is that the distance between $P_n$ and $A_n$ is at most 1. (iii) The hunter moves visibly to a point $B_n$ such that the distance between $B_{n-1}$ and $B_n$ is exactly 1. Is it always possible, no matter how the rabbit moves, and no matter what points are reported by the tracking device, for the hunter to choose her moves so that after $10^9$ rounds she can ensure that the distance between her and the rabbit is at most 100?
Answer: false

Lean formal statement:
import Mathlib

theorem imo_2017_p3 (start : EuclideanSpace ℝ (Fin 2)) : ((false) : Bool ) =
    ∀ (A : ℕ → EuclideanSpace ℝ (Fin 2)),
      A 0 = (fun x => if x = 0 then start 1 else start 2) →
      ∀ n, dist (A n) (A (n + 1)) = 1 →
      (∃ (P : ℕ → EuclideanSpace ℝ (Fin 2)), ∀ n > 0, dist (P n) (A n) ≤ 1) →
      (∃ (B : ℕ → EuclideanSpace ℝ (Fin 2)),
        B 0 = (fun x => if x = 0 then start 1 else start 2) ∧ ∀ n, dist (B n) (B (n + 1)) = 1 ∧
        dist (A (10 ^ 9)) (B (10 ^9)) ≤ 100) := by sorry
Problem: An integer $N \ge 2$ is given. A collection of $N(N + 1)$ soccer players, no two of whom are of the same height, stand in a row. Sir Alex wants to remove $N(N - 1)$ players from this row leaving a new row of $2N$ players in which the following $N$ conditions hold: ($1$) no one stands between the two tallest players, ($2$) no one stands between the third and fourth tallest players, $\cdots$ ($N$) no one stands between the two shortest players. Show that this is always possible.

Lean formal statement:
import Mathlib

open Equiv Finset

theorem imo_2017_p5 (N : ℕ) (h_N : N ≥ 2) (height : Perm (Fin (N * (N + 1)))) :
    ∃ kept : Fin (2 * N) ↪o Fin (N * (N + 1)),
    
    ∀ i j, Even #{l | height (kept l) < height (kept i)} →
      
      #{l | height (kept l) < height (kept i)} + 1 = #{l | height (kept l) < height (kept j)} →
        
         (¬ ∃ k, (i < k ∧ k < j) ∨ (j < k ∧ k < i)) := by sorry
Problem: An anti-Pascal triangle is an equilateral triangular array of numbers such that, except for the numbers in the bottom row, each number is the absolute value of the difference of the two numbers immediately below it. For example, the following is an anti-Pascal triangle with four rows which contains every integer from $1$ to $10$ \[4\]\[2\quad 6\]\[5\quad 7 \quad 1\] \[8\quad 3 \quad 10 \quad 9\] Does there exist an anti-Pascal triangle with $2018$ rows which contains every integer from $1$ to $1 + 2 + 3 + \dots + 2018$?
Answer: false

Lean formal statement:
import Mathlib

structure PascalIndex (n : ℕ) where
  (i : ℕ) (j : ℕ)
  (i_le_n : i ≤ n)
  (j_le_i : j < i)

def IsAntiPascal (n : ℕ) (values : PascalIndex n → ℤ) : Prop :=
  ∀ index : PascalIndex n,
    if h : index.i < n then
      values index =
        abs (
          values { i := index.i + 1, j := index.j, i_le_n := by omega, j_le_i := by linarith [index.j_le_i] } -
          - values { i := index.i + 1, j := index.j + 1, i_le_n := by omega, j_le_i := by linarith [index.j_le_i] }
        )
    else
      true

theorem imo_2018_p3 : ((false) : Bool ) = ∃ values, IsAntiPascal 2018 values ∧
    Finset.Icc (1 : ℤ) (∑ i ∈ Finset.Icc 1 2018, i) = {x | ∃ i, x = values i} := by sorry
Problem: A site is any point $(x, y)$ in the plane such that $x$ and $y$ are both positive integers less than or equal to 20. Initially, each of the 400 sites is unoccupied. Amy and Ben take turns placing stones with Amy going first. On her turn, Amy places a new red stone on an unoccupied site such that the distance between any two sites occupied by red stones is not equal to $\sqrt{5}$. On his turn, Ben places a new blue stone on any unoccupied site. (A site occupied by a blue stone is allowed to be at any distance from any other occupied site.) They stop as soon as a player cannot place a stone. Find the greatest $K$ such that Amy can ensure that she places at least $K$ red stones, no matter how Ben places his blue stones.
Answer: 100

Lean formal statement:
import Mathlib

abbrev Site := Fin 20 × Fin 20

def Site.asPoint (s : Site) : EuclideanSpace ℝ (Fin 2) :=
  fun x => if x = 0 then (s.1.val + 1) else (s.2.val + 1)

inductive State
  | red
  | blue
  | unoccupied

abbrev Game := Site → State

def initialGame : Game := fun _ => State.unoccupied

def valid_Amy_move (x : Site) (g : Game) : Prop :=
  g x = State.unoccupied ∧
  ∀ y, g y = State.red → dist x.asPoint y.asPoint ≠ √5

def valid_Ben_move (x : Site) (g : Game) : Prop :=
  g x = State.unoccupied

def AmyStrategy := Π (g : Game), Option ((x : Site) ×' valid_Amy_move x g)

def Game.updateAccordingToAmyStrategy (g : Game) (s : AmyStrategy) : Option Game :=
  (s g) >>= fun p => .some <| Function.update g p.1 .red

def BenStrategy := Π (g : Game), Option ((x : Site) ×' valid_Ben_move x g)

def Game.updateAccordingToBenStrategy (g : Game) (s : BenStrategy) : Option Game :=
  (s g) >>= fun p => .some <| Function.update g p.1 .blue

def updateOneTurn (a : AmyStrategy) (b : BenStrategy) (g : Game) : Option Game :=
  g.updateAccordingToAmyStrategy a >>= fun g' => g'.updateAccordingToBenStrategy b

def updateGame (a : AmyStrategy) (b : BenStrategy) (g : Game) : ℕ → Option Game
  | 0 => .some g
  | (n + 1) => updateOneTurn a b g >>= (updateGame a b · n)

def CanPlaceKRedStones (a : AmyStrategy) (b : BenStrategy) : ℕ → Prop
  | 0 => True 
  | n+1 => 
    ∃ (h : updateGame a b initialGame n |>.isSome), 
      a ((updateGame a b initialGame n).get h) |>.isSome 

theorem imo_2018_p4 :
    
    (∃ a : AmyStrategy, ∀ b : BenStrategy, CanPlaceKRedStones a b ((100) : ℕ )) ∧
    
    (∀ a : AmyStrategy, ∃ b : BenStrategy, ¬ CanPlaceKRedStones a b (((100) : ℕ ) + 1)) := by
    sorry
Problem: The Bank of Bath issues coins with an $H$ on one side and a $T$ on the other. Harry has $n$ of these coins arranged in a line from left to right. He repeatedly performs the following operation: If there are exactly $k > 0$ coins showing $H$, then he turns over the $k^{th}$ coin from the left; otherwise, all coins show $T$ and he stops. For example, if $n = 3$ the process starting with the configuration $THT$ would be $THT \rightarrow HHT \rightarrow HTT \rightarrow TTT$, which stops after three operations. (a) Show that, for each initial configuration, Harry stops after a finite number of operations. (b) For each initial configuration $C$, let $L(C)$ be the number of operations before Harry stops. For example, $L(THT) = 3$ and $L(TTT) = 0$. Determine the average value of $L(C)$ over all $2^n$ possible initial configurations $C$.
Answer: fun n => n * (n + 1) / 4

Lean formal statement:
import Mathlib

abbrev Coin := Fin 2

abbrev Coin.H : Coin := 0

abbrev Coin.T : Coin := 1

abbrev CoinConfig (n : ℕ) := Fin n → Coin

def CoinConfig.countH {n : ℕ} (c : CoinConfig n) : ℕ := (List.ofFn c).count .H

def CoinConfig.flip {n : ℕ} (c : CoinConfig n) (k : ℕ) : CoinConfig n :=
  fun i => if i.val + 1 = k then
    match c i with
    | .H => .T
    | .T => .H
  else c i

def CoinConfig.update {n : ℕ} (c : CoinConfig n) : Option (CoinConfig n) :=
  if c.countH = 0 then none else .some <| c.flip c.countH

def CoinConfig.updateMultipleTimes {n : ℕ} (c : CoinConfig n) : ℕ → Option (CoinConfig n)
  | 0 => if c.countH = 0 then none else .some c
  | k+1 => c.updateMultipleTimes k >>= update

theorem imo_2019_p5_1 {n : ℕ} (hn : n > 0) : ∀ (c : CoinConfig n), ∃ N : ℕ, c.updateMultipleTimes N = .none := by sorry

theorem imo_2019_p5_2 {n : ℕ} (hn : n > 0) : ((fun n => n * (n + 1) / 4) : ℕ → ℚ ) n =
    ∑ c : CoinConfig n, (Nat.find (imo_2019_p5_1 hn c) : ℚ) / (Fintype.card (CoinConfig n)) := by sorry
Problem: There is an integer $n > 1$. There are $n^2$ stations on a slope of a mountain, all at different altitudes. Each of two cable car companies, $A$ and $B$, operates $k$ cable cars; each cable car provides a transfer from one of the stations to a higher one (with no intermediate stops). The $k$ cable cars of $A$ have $k$ different starting points and $k$ different finishing points, and a cable car that starts higher also finishes higher. The same conditions hold for $B$. We say that two stations are linked by a company if one can start from the lower station and reach the higher one by using one or more cars of that company (no other movements between stations are allowed). Determine the smallest positive integer k for which one can guarantee that there are two stations that are linked by both companies.
Answer: fun n => n ^ 2 - n + 1

Lean formal statement:
import Mathlib

def Iscompanies (n k : ℕ) (car_set : Finset (Fin n × Fin n)) : Prop :=
  car_set.card = k ∧
  (∀ (a b : Fin n), (a, b) ∈ car_set → a < b)∧
  (∀ a ∈ car_set, ∀ b ∈ car_set, a ≠ b → a.1 ≠ b.1 ∧ a.2 ≠ b.2)

def Islinked {n : ℕ} (a b : Fin n) (car_set : Finset (Fin n × Fin n)) : Prop :=
  ∃ s : List (Fin n × Fin n), s.Nodup ∧ (∀ i ∈ s, (i ∈ car_set ∧
  (List.foldl (fun x y => if x.2 = y.1 then (x.1, y.2) else x) (a, a) s = (a, b))))

def Condition (n k : ℕ) : Prop :=
  ∃ (companyA companyB : Finset (Fin n × Fin n)), Iscompanies n k companyA ∧ Iscompanies n k companyB ∧
  (∃ (a b : Fin n), a ≠ b ∧ Islinked a b companyA ∧ Islinked a b companyB)

theorem imo_2020_p4 (n : ℕ) (hn : n > 1) : IsLeast {k | Condition n k} (((fun n => n ^ 2 - n + 1) : ℕ → ℕ ) n) := by sorry
Problem: Two squirrels, Bushy and Jumpy, have collected 2021 walnuts for the winter. Jumpy numbers the walnuts from 1 through 2021, and digs 2021 little holes in a circular pattern in the ground around their favourite tree. The next morning Jumpy notices that Bushy had placed one walnut into each hole, but had paid no attention to the numbering. Unhappy, Jumpy decides to reorder the walnuts by performing a sequence of 2021 moves. In the $k$-th move, Jumpy swaps the positions of the two walnuts adjacent to walnut $k$. Prove that there exists a value of $k$ such that, on the $k$-th move, Jumpy swaps some walnuts $a$ and $b$ such that $a < k < b$.

Lean formal statement:
import Mathlib

def move (k : Fin 2021) (order : Fin 2021 ≃ Fin 2021) : Fin 2021 ≃ Fin 2021 :=
  
  order.trans (Equiv.swap (order (finRotate _ (order.symm k))) (order ((finRotate _).symm (order.symm k))))

def performMoves (originalOrder : Fin 2021 ≃ Fin 2021) : (Fin 2021) → (Fin 2021 ≃ Fin 2021)
  | 0 => originalOrder
  | ⟨n + 1, lt⟩ => move n (performMoves originalOrder ⟨n, lt_trans (by omega) lt⟩)

theorem imo_2021_p5 (originalOrder : Fin 2021 ≃ Fin 2021) :
    ∃ k, min (finRotate _ ((performMoves originalOrder k).symm k) : ℕ)
        ((finRotate _).symm ((performMoves originalOrder k).symm k) : ℕ) < (k : ℕ) ∧
      (k : ℕ) < max (finRotate _ ((performMoves originalOrder k).symm k) : ℕ)
        ((finRotate _).symm ((performMoves originalOrder k).symm k) : ℕ) := by sorry
Problem: The Bank of Oslo issues two types of coin: aluminium (denoted A) and bronze (denoted B). Marianne has $n$ aluminium coins and $n$ bronze coins, arranged in a row in some arbitrary initial order. A chain is any subsequence of consecutive coins of the same type. Given a fixed positive integer $k\le 2n$, Marianne repeatedly performs the following operation: she identifies the longest chain containing the $k^{th}$ coin from the left, and moves all coins in that chain to the left end of the row. For example, if $n = 4$ and $k = 4$, the process starting from the ordering AABBBABA would be $AABBBABA \rightarrow BBBAAABA \rightarrow AAABBBBA \rightarrow BBBBAAAA \rightarrow BBBBAAAA \rightarrow \ldots$. Find all pairs $(n, k)$ with $1 \le k \le 2n$ such that for every initial ordering, at some moment during the process, the leftmost $n$ coins will all be of the same type.
Answer: fun n => {p | p.1 = n ∧ n ≤ p.2 ∧ p.2 ≤ ⌈(3 * n : ℝ) / 2⌉₊}

Lean formal statement:
import Mathlib

abbrev sortedList (n : ℕ) := (List.range (2 * n))|>.map
  (fun i ↦ if i < n then 0 else 1)

def checkList (k : ℕ) : List ℕ → ℕ × ℕ := fun L ↦ Id.run do
  let mut i0 := k - 1
  let mut i1 := k - 1
  for i in [k : L.length] do
    if L[i]! = L[k-1]! then
      i1 := i1 + 1
    else break
  for j in [1 : k] do
    if L[k-1-j]! = L[k-1]! then
      i0 := i0 - 1
    else break
  return (i0, i1)

abbrev action (k : ℕ) : List ℕ → List ℕ := fun L ↦
  (List.range ((checkList k L).2 - (checkList k L).1 + 1)).map (fun _ ↦ L[k-1]!) ++
  (List.range (checkList k L).1).map (fun i ↦ L[i]!) ++
  (List.range (L.length - (checkList k L).2 - 1)).map (fun i ↦ L[i + (checkList k L).2 + 1]!)

abbrev pown (k m : ℕ) : List ℕ → List ℕ := fun L ↦ Id.run do
  let mut L' := L
  for _ in [0 : m] do
    L' := action k L'
  return L'

abbrev checkLeft (n : ℕ) : List ℕ → Bool := fun L ↦ Id.run do
  for i in [0 : n] do
    if L[i]! ≠ L[0]! then
      return false
    else continue
  return true

def initial (n : ℕ) : Finset (List ℕ) := (List.replicate n 0 ++ List.replicate n 1).permutations.toFinset

 theorem imo_2022_p1 (n : ℕ) (hn : n > 0) :
    {(n', k) | n = n' ∧ k ≥ 1 ∧ k ≤ 2 * n ∧ (∀ I ∈ initial n, ∃ m : ℕ, checkLeft n' (pown k m I))} =
    ((fun n => {p | p.1 = n ∧ n ≤ p.2 ∧ p.2 ≤ ⌈(3 * n : ℝ) / 2⌉₊}) : ℕ → Set (ℕ × ℕ) ) n := by sorry
Problem: Let $n$ be a positive integer. A Japanese triangle consists of $1 + 2 + \dots + n$ circles arranged in an equilateral triangular shape such that for each $i = 1$, $2$, $\dots$, $n$, the $i^{th}$ row contains exactly $i$ circles, exactly one of which is coloured red. A ninja path in a Japanese triangle is a sequence of $n$ circles obtained by starting in the top row, then repeatedly going from a circle to one of the two circles immediately below it and finishing in the bottom row. In terms of $n$, find the greatest $k$ such that in each Japanese triangle there is a ninja path containing at least $k$ red circles.
Answer: fun n => ⌊Real.logb 2 n⌋₊ + 1

Lean formal statement:
import Mathlib

structure Index (n : ℕ+) where
  row : ℕ
  col : ℕ
  
  le_row : 1 ≤ row
  row_le : row ≤ n
  
  le_col : 1 ≤ col
  col_le : col ≤ row

def Index.atBottomLeft {n : ℕ+} (p q : Index n) : Prop :=
  q.row + 1 = p.row ∧ q.col = p.col

def Index.atBottomRight {n : ℕ+} (p q : Index n) : Prop :=
  q.row + 1 = p.row ∧ q.col + 1 = p.col

@[simps]
def triangleGraph (n : ℕ+) : Digraph (Index n) where
  Adj p q :=
    p.atBottomLeft q ∨ p.atBottomRight q ∨
    q.atBottomLeft p ∨ q.atBottomRight p

abbrev JapaneseTriangle (n : ℕ+) := ∀ (i : Fin n), Fin (i + 1)

structure NinjaPath {n : ℕ+} (jt : JapaneseTriangle n) where
  path : RelSeries (triangleGraph n |>.Adj)
  length : path.length = n.natPred

@[simp]
lemma NinjaPath.path_length_succ {n : ℕ+} {jt : JapaneseTriangle n} (p : NinjaPath jt) :
    p.path.length + 1 = n := by
  simp [p.length]

def NinjaPath.countRed {n : ℕ+} {jt : JapaneseTriangle n} (p : NinjaPath jt) : ℕ :=
  ∑ (i : Fin (p.path.length + 1)),
    if (jt (Fin.cast (by simp) i) : ℕ) = (p.path i).col
    then 1
    else 0

theorem imo_2023_p5 (n : ℕ+) :
    IsGreatest {k | ∀ (jt : JapaneseTriangle n), ∃ (p : NinjaPath jt), k ≤ p.countRed}
    (((fun n => ⌊Real.logb 2 n⌋₊ + 1) : ℕ+ → ℕ ) n) := by sorry
Problem: Turbo the snail plays a game on a board with 2024 rows and 2023 columns. There are hidden monsters in 2022 of the cells. Initially, Turbo does not know where any of the monsters are, but he knows that there is exactly one monster in each row except the first row and the last row, and that each column contains at most one monster. Turbo makes a series of attempts to go from the first row to the last row. On each attempt, he chooses to start on any cell in the first row, then repeatedly moves to an adjacent cell sharing a common side. (He is allowed to return to a previously visited cell.) If he reaches a cell with a monster, his attempt ends and he is transported back to the first row to start a new attempt. The monsters do not move, and Turbo remembers whether or not each cell he has visited contains a monster. If he reaches any cell in the last row, his attempt ends and the game is over. Determine the minimum value of $n$ for which Turbo has a strategy that guarantees reaching the last row on the $n^{th}$ attempt or earlier, regardless of the locations of the monsters.
Answer: 3

Lean formal statement:
import Mathlib

namespace Imo_2024_p5

abbrev Cell (N : ℕ) : Type := Fin (N + 2) × Fin (N + 1)

abbrev InteriorRow (N : ℕ) : Type := (Set.Icc 1 ⟨N, by omega⟩ : Set (Fin (N + 2)))

abbrev MonsterData (N : ℕ) : Type := InteriorRow N ↪ Fin (N + 1)

def MonsterData.monsterCells {N} (m : MonsterData N) :
    Set (Cell N) :=
  Set.range (fun x : InteriorRow N ↦ ((x : Fin (N + 2)), m x))

def Adjacent {N} (x y : Cell N) : Prop :=
  Nat.dist x.1 y.1 + Nat.dist x.2 y.2 = 1

structure Path (N : ℕ) where
  
  cells : List (Cell N)
  nonempty : cells ≠ []
  head_first_row : (cells.head nonempty).1 = 0
  last_last_row : (cells.getLast nonempty).1 = N + 1
  valid_move_seq : cells.Chain' Adjacent

noncomputable def Path.firstMonster {N} (p : Path N) (m : MonsterData N) : Option (Cell N) :=
  letI := Classical.propDecidable
  p.cells.find? (fun x ↦ (x ∈ m.monsterCells : Bool))

abbrev Strategy (N : ℕ) : Type := ⦃k : ℕ⦄ → (Fin k → Option (Cell N)) → Path N

noncomputable def Strategy.play {N} (s : Strategy N) (m : MonsterData N) :
    (k : ℕ) → Fin k → Option (Cell N)
  | 0 => Fin.elim0
  | k + 1 => Fin.snoc (s.play m k) ((s (s.play m k)).firstMonster m)

def Strategy.WinsIn {N} (s : Strategy N) (m : MonsterData N) (k : ℕ) : Prop :=
  none ∈ Set.range (s.play m k)

def Strategy.ForcesWinIn {N} (s : Strategy N) (k : ℕ) : Prop :=
  ∀ m, s.WinsIn m k

theorem imo_2024_p5 : IsLeast {k | ∃ s : Strategy 2022, s.ForcesWinIn k} ((3) : ℕ ) := by
    sorry