AI-MO/CombiBench huggingface dataset:
Problem: In a mathematical competition, in which 6 problems were posed to the participants, every two of these problems were solved by more than 2/5 of the contestants. Moreover, no contestant solved all the 6 problems. Show that there are at least 2 contestants who solved exactly 5 problems each.

Lean formal statement:
import Mathlib

theorem imo_2005_p6 {participants : Type} [Fintype participants] [DecidableEq participants]
    (solved : Fin 6 → Finset participants)
    (h : ∀ i j, i ≠ j → (solved i ∩ solved j).card > (2 * Fintype.card participants : ℝ) / 5)
    (h' : ∀ i : participants, ∃ p : Fin 6, i ∉ solved p) :
    ∃ s : Finset participants, s.card ≥ 2 ∧
    (∀ i ∈ s, ∃ p : Finset (Fin 6), p.card = 5 ∧ ∀ j, j ∈ p ↔ i ∈ solved j) := by sorry
Problem: Let $P$ be a regular 2006-gon. A diagonal of $P$ is called good if its endpoints divide the boundary of $P$ into two parts, each composed of an odd number of sides of $P$. The sides of $P$ are also called good. Suppose $P$ has been dissected into triangles by 2003 diagonals, no two of which have a common point in the interior of $P$. Find the maximum number of isosceles triangles having two good sides that could appear in such a configuration.
Answer: 1003

Lean formal statement:
import Mathlib

open scoped Classical Finset

instance {N : ℕ} : CircularOrder (Fin N) := LinearOrder.toCircularOrder _

variable {α : Type*} [CircularOrder α] {a b c d : α}

def SBtw₄ (a b c d : α) : Prop := sbtw a b c ∧ sbtw c d a

lemma sbtw₄_swap : SBtw₄ a b c d ↔ SBtw₄ c d a b := and_comm

variable {N : ℕ}

abbrev Diagonal (N : ℕ) := {e : Sym2 (Fin N) // ¬ e.IsDiag}

namespace Diagonal

def Intersect (d₁ d₂ : Diagonal N) : Prop :=
  Sym2.lift₂ {
    val a b c d := SBtw₄ a c b d ∨ SBtw₄ a d b c
    property a b c d := by
      simp only [eq_iff_iff]; constructor <;> rw [sbtw₄_swap, or_comm, sbtw₄_swap]
  } d₁.1 d₂.1

def Good (d : Diagonal N) : Prop :=
  Sym2.lift {
    val a b := Odd (a.val + b.val : ℕ)
    property a b := by simp [add_comm]
  } d.1

end Diagonal

structure TriangleDissection (N : ℕ) where
  diagonals : Fin (2 * N - 3) ↪ Diagonal N
  pairwise_not_intersect_diagonals : Pairwise fun i j ↦ ¬ (diagonals i).Intersect (diagonals j)

noncomputable def TriangleDissection.numOfIsoscelesTriangle (C : TriangleDissection N) : ℕ := by
  classical exact
  #{(a, b, c) : Fin N × Fin N × Fin N |
    ∃ (hab : a < b) (hbc : b < c),
      
      (∃ i, C.diagonals i = s(a, b)) ∧
      (∃ i, C.diagonals i = s(b, c)) ∧
      (∃ i, C.diagonals i = s(c, a)) ∧
      
      ( Diagonal.Good ⟨s(a, b), by simpa using hab.ne⟩ ∧
        Diagonal.Good ⟨s(b, c), by simpa using hbc.ne⟩ ∨
        Diagonal.Good ⟨s(b, c), by simpa using hbc.ne⟩ ∧
        Diagonal.Good ⟨s(c, a), by simpa using (hab.trans hbc).ne'⟩ ∨
        Diagonal.Good ⟨s(c, a), by simpa using (hab.trans hbc).ne'⟩ ∧
        Diagonal.Good ⟨s(a, b), by simpa using hab.ne⟩) ∧
      
      ((b.val - a.val : ℤ) = c.val - b.val ∨
       (c.val - b.val : ℤ) = N + a.val - c.val ∨
       (N + a.val - c.val : ℤ) = b.val - a.val)}

theorem imo_2006_p2 :
    IsGreatest {k | ∃ c : TriangleDissection 2006, c.numOfIsoscelesTriangle = k}
      ((1003) : ℕ ) :=  by sorry
Problem: In a mathematical competition some competitors are friends. Friendship is always mutual. Call a group of competitors a clique if each two of them are friends. (In particular, any group of fewer than two competitors is a clique.) The number of members of a clique is called its size. Given that, in this competition, the largest size of a clique is even, prove that the competitors can be arranged in two rooms such that the largest size of a clique contained in one room is the same as the largest size of a clique contained in the other room.

Lean formal statement:
import Mathlib

theorem imo_2007_p3 {player : Type} [Fintype player] (math_competiton : SimpleGraph player)
    (h : Even math_competiton.cliqueNum) :
    ∃ a : SimpleGraph.Subgraph math_competiton, a.coe.cliqueNum = aᶜ.coe.cliqueNum := by sorry
Problem: Let $n$ and $k$ be positive integers with $k \geq n$ and $k - n$ an even number. Let $2n$ lamps labelled $1$, $2$, ..., $2n$ be given, each of which can be either on or off. Initially all the lamps are off. We consider sequences of steps: at each step one of the lamps is switched (from on to off or from off to on). Let $N$ be the number of such sequences consisting of $k$ steps and resulting in the state where lamps $1$ through $n$ are all on, and lamps $n + 1$ through $2n$ are all off. Let $M$ be number of such sequences consisting of $k$ steps, resulting in the state where lamps $1$ through $n$ are all on, and lamps $n + 1$ through $2n$ are all off, but where none of the lamps $n + 1$ through $2n$ is ever switched on. Determine $\frac{N}{M}$.
Answer: fun n k => 2 ^ (k.1 - n.1)

Lean formal statement:
import Mathlib

def switch_lamp (n : ℕ+) (switch_label : Fin (2 * n)) (lamps_state : List Bool) : List Bool :=
  List.mapIdx (fun j (x : Bool) => if j = switch_label then ¬x else x) lamps_state

def lamps_final_state (n : ℕ+) (switch_list : List (Fin (2 * n))) : List Bool :=
  match switch_list with
  | [] => (List.ofFn (fun _ : Fin (2 * n) => false))
  | h :: t => switch_lamp n h (lamps_final_state n t)

def final_goal (n : ℕ+) := List.ofFn (fun (i : Fin (2 * n)) => if i < n then true else false)

def N (n k : ℕ+) := @Finset.univ (Fin k → Fin (2 * n)) _ |>.filter
  (fun f => lamps_final_state n (List.ofFn f) = final_goal n) |>.card

def M (n k : ℕ+) := @Finset.univ (Fin k → Fin (2 * n)) _ |>.filter
  (fun f => ∀ (i : Fin k), f i < (n : Fin (2 * n))) |>.filter
  (fun f => lamps_final_state n (List.ofFn f) = final_goal n) |>.card

theorem imo_2008_p5 (n k : ℕ+) (hnk : k ≥ n) (hnk' : Even (k - n)) :
    N n k / M n k = ((fun n k => 2 ^ (k.1 - n.1)) : ℕ+ → ℕ+ → ℝ ) n k := by sorry
Problem: Each of the six boxes $B_1$, $B_2$, $B_3$, $B_4$, $B_5$, $B_6$ initially contains one coin. The following operations are allowed: Type 1) Choose a non-empty box $B_j$, $1\leq j \leq 5$, remove one coin from $B_j$ and add two coins to $B_{j+1}$; Type 2) Choose a non-empty box $B_k$, $1\leq k \leq 4$, remove one coin from $B_k$ and swap the contents (maybe empty) of the boxes $B_{k+1}$ and $B_{k+2}$. Determine if there exists a finite sequence of operations of the allowed types, such that the five boxes $B_1$, $B_2$, $B_3$, $B_4$, $B_5$ become empty, while box $B_6$ contains exactly $2010^{2010^{2010}}$ coins.
Answer: true

Lean formal statement:
import Mathlib

structure Boxes where
  (B1 B2 B3 B4 B5 B6 : ℕ)

def op11 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1 - 1, b2 + 2, b3, b4, b5, b6⟩

def op12 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2 - 1, b3 + 2, b4, b5, b6⟩

def op13 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2, b3 - 1, b4 + 2, b5, b6⟩

def op14 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2, b3, b4 - 1, b5 + 2, b6⟩

def op15 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2, b3, b4, b5 - 1, b6 + 2⟩

def op21 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1 - 1, b3, b2, b4, b5, b6⟩

def op22 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2 - 1, b4, b3, b5, b6⟩

def op23 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2, b3 - 1, b5, b4, b6⟩

def op24 : Boxes → Boxes
  | ⟨b1, b2, b3, b4, b5, b6⟩ => ⟨b1, b2, b3, b4 - 1, b6, b5⟩

inductive OP
  | op11 | op12 | op13 | op14 | op15 | op21 | op22 | op23 | op24

def apply_op : OP → (Boxes → Boxes)
  | OP.op11 => op11
  | OP.op12 => op12
  | OP.op13 => op13
  | OP.op14 => op14
  | OP.op15 => op15
  | OP.op21 => op21
  | OP.op22 => op22
  | OP.op23 => op23
  | OP.op24 => op24

def init : Boxes := ⟨1, 1, 1, 1, 1, 1⟩

theorem imo_2010_p5 : ((true) : Bool ) = (∃ seq : List OP,
    (seq.map apply_op).foldl (· ∘ ·) id init = ⟨0, 0, 0, 0, 0, 2010 ^ (2010 ^ 2010)⟩) := by sorry
Problem: Let $\mathcal{S}$ be a finite set of at least two points in the plane. Assume that no three points of $\mathcal S$ are collinear. A windmill is a process that starts with a line $\ell$ going through a single point $P \in \mathcal S$. The line rotates clockwise about the pivot $P$ until the first time that the line meets some other point belonging to $\mathcal S$. This point, $Q$, takes over as the new pivot, and the line now rotates clockwise about $Q$, until it next meets a point of $\mathcal S$. This process continues indefinitely. Show that we can choose a point $P$ in $\mathcal S$ and a line $\ell$ going through $P$ such that the resulting windmill uses each point of $\mathcal S$ as a pivot infinitely many times.

Lean formal statement:
import Mathlib

open EuclideanGeometry Real Filter

namespace List

variable {α β : Type*}

@[mk_iff]
inductive Triplewise (p : α → α → α → Prop) : List α → Prop
  | nil : [].Triplewise p
  | cons {a : α} {l : List α} : l.Pairwise (p a) → l.Triplewise p → (a :: l).Triplewise p

end List

instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2) := ⟨by simp⟩

variable {n} [Fintype n] [DecidableEq n]

noncomputable instance : Module.Oriented ℝ (EuclideanSpace ℝ n) n where
  positiveOrientation := Basis.orientation (Pi.basisFun ℝ n)

structure IsWindmillProcess (S : Set (EuclideanSpace ℝ (Fin 2)))
    (f : ℕ → EuclideanSpace ℝ (Fin 2)) where
  forall_mem n : f n ∈ S
  oangle_le_oangle n x : x ∈ S →
    toIocMod two_pi_pos 0 (oangle (f n) (f (n + 1)) (f (n + 2))).toReal
      ≤ toIocMod two_pi_pos 0 (oangle (f n) (f (n + 1)) x).toReal

theorem imo_2011_p2 (l : List (EuclideanSpace ℝ (Fin 2)))
    (hl : l.Triplewise (¬ Collinear ℝ {·, ·, ·})) :
    ∃ f : ℕ → EuclideanSpace ℝ (Fin 2),
      IsWindmillProcess {x | x ∈ l} f ∧ ∀ x ∈ l, ∃ᶠ n in atTop, f n = x := by sorry
Problem: Let $n > 0$ be an integer. We are given a balance and $n$ weights of weight $2^0,2^1, \cdots ,2^{n-1}$. We are to place each of the $n$ weights on the balance, one after another, in such a way that the right pan is never heavier than the left pan. At each step we choose one of the weights that has not yet been placed on the balance, and place it on either the left pan or the right pan, until all of the weights have been placed. Determine the number of ways in which this can be done.
Answer: fun n => Nat.doubleFactorial (2 * n - 1)

Lean formal statement:
import Mathlib

def weight_of_left_pan {n : ℕ} (σ : Equiv.Perm (Fin n)) (place_left : Fin n → Bool) (step : ℕ) : ℕ :=
  ∑ j with place_left j = true ∧ σ j ≤ step, 2 ^ j.1

def weight_of_right_pan {n : ℕ} (σ : Equiv.Perm (Fin n)) (place_left : Fin n → Bool) (step : ℕ) : ℕ :=
  ∑ j with place_left j = false ∧ σ j ≤ step, 2 ^ j.1

def is_valid_placement {n : ℕ} (σ : Equiv.Perm (Fin n)) (place_left : Fin n → Bool) : Prop :=
  ∀ step : Fin n, weight_of_right_pan σ place_left step ≤ weight_of_left_pan σ place_left step

instance {n : ℕ} (σ : Equiv.Perm (Fin n)) (place_left : Fin n → Bool) :
  Decidable (is_valid_placement σ place_left) := by
  simp [is_valid_placement]; infer_instance

abbrev all_placements (n : ℕ) :=
  Finset.product (@Finset.univ (Equiv.Perm (Fin n)) _) (@Finset.univ (Fin n → Bool) _)

abbrev valid_placements (n : ℕ) :=
  all_placements n |>.filter (fun (σ, f) => is_valid_placement σ f)

theorem imo_2011_p4 (n : ℕ) (hn : n > 0) :
    (valid_placements n).card = ((fun n => Nat.doubleFactorial (2 * n - 1)) : ℕ → ℕ ) n := by sorry
Problem: The liar’s guessing game is a game played between two players A and B. The rules of the game depend on two positive integers $k$ and $n$ which are known to both players. At the start of the game the player A chooses integers $x$ and $N$ with $1 \le x \le N$. Player A keeps $x$ secret, and truthfully tells $N$ to the player B. The player B now tries to obtain information about $x$ by asking player A questions as follows: each question consists of B specifying an arbitrary set $S$ of positive integers (possibly one specified in some previous question), and asking A whether $x$ belongs to $S$. Player B may ask as many questions as he wishes. After each question, player A must immediately answer it with yes or no, but is allowed to lie as many times as she wants; the only restriction is that, among any $k+1$ consecutive answers, at least one answer must be truthful. After B has asked as many questions as he wants, he must specify a set $X$ of at most $n$ positive integers. If $x \in X$, then B wins; otherwise, he loses. Prove that: (a) If $n \ge 2^k$ then B has a winning strategy. (b) There exists a positive integer $k_0$ such that for every $k \ge k_0$ there exists an integer $n \ge 1.99^k$ for which B cannot guarantee a victory.

Lean formal statement:
import Mathlib

open scoped Finset

set_option autoImplicit false

structure AliceStrategy where
  
  N : ℕ
  
  x : Fin N
  
  nextAnswer : List (Set (Fin N) × Bool) → Set (Fin N) → Bool

structure BobStrategy where
  
  nextQuestion N : List (Set (Fin N) × Bool) → Set (Fin N)
  
  guess N : List (Set (Fin N) × Bool) → Finset (Fin N)

variable {k n : ℕ}

def history (A : AliceStrategy) (B : BobStrategy) : ℕ → List (Set (Fin A.N) × Bool)
  | 0 => []
  | t + 1 =>
    (B.nextQuestion A.N (history A B t),
      A.nextAnswer (history A B t) (B.nextQuestion A.N (history A B t)))
        :: history A B t

def AliceStrategy.IsValid (A : AliceStrategy) (B : BobStrategy) (k : ℕ) : Prop :=
  ∀ t₀ : ℕ, ∃ t ∈ Finset.Ico t₀ (t₀ + k),
    A.nextAnswer (history A B t) (B.nextQuestion A.N (history A B t))
      = (A.x ∈ B.nextQuestion A.N (history A B t))

def BobStrategy.IsValid (A : AliceStrategy) (B : BobStrategy) (n t : ℕ) : Prop :=
  #(B.guess A.N (history A B t)) ≤ n

def BobStrategy.IsWinning (B : BobStrategy) (k n : ℕ) : Prop :=
  ∀ (A : AliceStrategy), A.IsValid B k → ∃ t, B.IsValid A n t ∧ A.x ∈ B.guess A.N (history A B t)

theorem imo_2012_p3 :
    
    (∀ k n, 2 ^ k ≤ n → ∃ B : BobStrategy, B.IsWinning k n) ∧
    
    
      ∃ k₀,
        ∀ k ≥ k₀,
          ∃ n : ℕ, n ≥ (1.99 : ℝ) ^ k ∧
            ∀ B : BobStrategy, ¬ B.IsWinning k n := by sorry
Problem: A configuration of $4027$ points in the plane is called Colombian if it consists of $2013$ red points and $2014$ blue points, and no three of the points of the configuration are collinear. By drawing some lines, the plane is divided into several regions. An arrangement of lines is good for a Colombian configuration if the following two conditions are satisfied: (1) no line passes through any point of the configuration; (2)no region contains points of both colours. Find the least value of $k$ such that for any Colombian configuration of $4027$ points, there is a good arrangement of $k$ lines.
Answer: 2013

Lean formal statement:
import Mathlib

structure Colombian_config : Type where
  (R B : Finset (ℝ × ℝ))
  (hR : R.card = 2013)
  (hB : B.card = 2014)
  (hC : R ∩ B = ∅)
  (h_no_collinear : ∀ p ∈ R ∪ B, ∀ q ∈ R ∪ B, ∀ r ∈ R ∪ B, p ≠ q → p ≠ r → q ≠ r →
    ¬ ∃ t : ℝ, t ≠ 0 ∧ t * (q.1 - p.1) = (r.1 - p.1) ∧ t * (q.2 - p.2) = (r.2 - p.2))

def Good_arrange (C : Colombian_config) (L : Finset (ℝ × ℝ × ℝ)) : Prop :=
  (∀ l ∈ L, l.1 ≠ 0 ∨ l.2.1 ≠ 0) ∧
  (∀ p ∈ C.R ∪ C.B, ∀ l ∈ L, l.1 * p.1 + l.2.1 * p.2 + l.2.2 ≠ 0) ∧
    ¬ (∃ q ∈ C.R, ∃ p ∈ C.B, ∀ l ∈ L,
      Real.sign (l.1 * p.1 + l.2.1 * p.2 + l.2.2) = Real.sign (l.1 * q.1 + l.2.1 * q.2 + l.2.2))

theorem imo_2013_p2 : IsLeast
    {k | ∀ C : Colombian_config, ∃ L : Finset (ℝ × ℝ × ℝ), L.card = k ∧ Good_arrange C L}
    ((2013) : ℕ ) := by sorry
Problem: Let $n \ge 3$ be an integer, and consider a circle with $n + 1$ equally spaced points marked on it. Consider all labellings of these points with the numbers $0, 1, ... , n$ such that each label is used exactly once; two such labellings are considered to be the same if one can be obtained from the other by a rotation of the circle. A labelling is called beautiful if, for any four labels $a < b < c < d$ with $a + d = b + c$, the chord joining the points labelled $a$ and $d$ does not intersect the chord joining the points labelled $b$ and $c$. Let $M$ be the number of beautiful labelings, and let N be the number of ordered pairs $(x, y)$ of positive integers such that $x + y \le n$ and $\gcd(x, y) = 1$. Prove that\[ M = N + 1.\]

Lean formal statement:
import Mathlib

open Equiv Fintype Finset

def IsBeautiful {n} (e : Perm (Fin (n + 1))) : Prop :=
  ∀ ⦃a b⦄, a < b → ∀ ⦃c⦄, b < c → ∀ ⦃d⦄, c < d → a.val + d.val = b.val + c.val →
    
    e a < e b ∧ e b < e d ∧ e a < e c ∧ e c < e d ∨
    
    e d < e b ∧ e b < e a ∧ e d < e c ∧ e c < e a ∨
    
    e b < e a ∧ e a < e c ∧ e b < e d ∧ e d < e c ∨
    
    e c < e a ∧ e a < e b ∧ e c < e d ∧ e d < e b ∨
    
    e a < e b ∧ e a < e c ∧ e d < e b ∧ e d < e c ∨
    
    e b < e a ∧ e c < e a ∧ e b < e d ∧ e c < e d

instance {n} : DecidablePred (IsBeautiful (n := n)) := by unfold IsBeautiful; infer_instance

def M (n : ℕ) : ℕ := #{e : Perm (Fin (n + 1)) | IsBeautiful e} / (n + 1)

def N (n : ℕ) : ℕ := #{xy ∈ .Icc 1 n ×ˢ .Icc 1 n | xy.1 + xy.2 ≤ n ∧ xy.1.gcd xy.2 = 1}

theorem imo_2013_p6 (n : ℕ) (hn : n ≥ 3) : M n = N n + 1 := by sorry
Problem: Let $n\ge2$ be an integer. Consider an $n\times n$ chessboard consisting of $n^2$ unit squares. A configuration of $n$ rooks on this board is $\textit{peaceful}$ if every row and every column contains exactly one rook. Find the greatest positive integer $k$ such that, for each peaceful configuration of $n$ rooks, there is a $k\times k$ square which does not contain a rook on any of its $k^2$ squares.
Answer: fun n => ⌈√n⌉₊ - 1

Lean formal statement:
import Mathlib

structure peaceful_rooks (n : ℕ) : Type where
  carrier :  Matrix (Fin n) (Fin n) Bool
  is_peaceful_row : ∀ i, List.count true (List.ofFn (fun j => carrier i j)) = 1
  is_peaceful_col : ∀ j, List.count true (List.ofFn (fun i => carrier i j)) = 1
deriving Fintype

theorem imo_2014_p2 (n : ℕ) (hn : n ≥ 2) :
    IsGreatest {(k : ℕ) | (k > 0) ∧ ∀ r : peaceful_rooks n, ∃ i j : Fin n,
    i.val + k - 1 < n ∧ i.val + k - 1 < n ∧
    ∀ m n, m.val < k ∧ n.val < k → r.carrier (i + m) (j + n) = false}
    (((fun n => ⌈√n⌉₊ - 1) : ℕ → ℕ ) n) := by sorry
Problem: A set of lines in the plane is in $\textit{general position}$ if no two are parallel and no three pass through the same point. A set of lines in general position cuts the plane into regions, some of which have finite area; we call these its $\textit{finite regions}$. Prove that for all sufficiently large $n$, in any set of $n$ lines in general position it is possible to colour at least $\sqrt{n}$ of the lines blue in such a way that none of its finite regions has a completely blue boundary.

Lean formal statement:
import Mathlib

def General_position (L : Finset (ℝ × ℝ × ℝ)) : Prop :=
  (∀ l ∈ L, l.1 ≠ 0 ∨ l.2.1 ≠ 0) ∧
  (∀ l1 ∈ L, ∀ l2 ∈ L, l1 ≠ l2 → l1.1 * l2.2.1 ≠ l1.2.1 * l2.1) ∧
  (∀ l1 ∈ L, ∀ l2 ∈ L, ∀ l3 ∈ L, l1 ≠ l2 → l1 ≠ l3 → l2 ≠ l3 →
    (¬ ∃ (p : ℝ × ℝ), l1.1 * p.1 + l1.2.1 * p.2 + l1.2.2 = 0 ∧
      l2.1 * p.1 + l2.2.1 * p.2 + l2.2.2 = 0 ∧ l3.1 * p.1 + l3.2.1 * p.2 + l3.2.2 = 0))

def finite_regions (S : Set (ℝ × ℝ)) (L : Finset (ℝ × ℝ × ℝ)) : Prop :=
  S ≠ ∅ ∧ (∃ a b : ℝ, ∀ p ∈ S, |p.1| ≤ a ∧ |p.2| ≤ b) ∧ (∀ p ∈ S, ∀ q ∈ S, p ≠ q → ∀ l ∈ L,
    Real.sign (l.1 * p.1 + l.2.1 * p.2 + l.2.2) = Real.sign (l.1 * q.1 + l.2.1 * q.2 + l.2.2))

theorem imo_2014_p6 : ∀ᶠ n in Filter.atTop,
    ∀ (L : Finset (ℝ × ℝ × ℝ)), General_position L ∧ L.card = n →
    ∃ B ≤ L, B.card ≥ Nat.sqrt n ∧ ∀ S ≤ B, ∀ (R : Set (ℝ × ℝ)), ¬finite_regions R S := by sorry
Problem: We say that a finite set $\mathcal{S}$ in the plane is balanced if, for any two different points $A$, $B$ in $\mathcal{S}$, there is a point $C$ in $\mathcal{S}$ such that $AC=BC$. We say that $\mathcal{S}$ is centre-free if for any three points $A$, $B$, $C$ in $\mathcal{S}$, there is no point $P$ in $\mathcal{S}$ such that $PA=PB=PC$. (1) Show that for all integers $n\geq 3$, there exists a balanced set consisting of $n$ points. (1) Determine all integers $n\geq 3$ for which there exists a balanced centre-free set consisting of $n$ points.
Answer: {n | n ≥ 3 ∧ Odd n}

Lean formal statement:
import Mathlib

def balanced (S : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
  ∀ A ∈ S, ∀ B ∈ S, A ≠ B → (∃ C ∈ S, dist A C = dist B C)

def centre_free (S : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
  ∀ A ∈ S, ∀ B ∈ S, ∀ C ∈ S, A ≠ B → B ≠ C → A ≠ C →
    ¬ (∃ P ∈ S, dist A P = dist B P ∧ dist B P = dist C P)

theorem imo_2015_p1 : (∀ n ≥ 3, ∃ (S : Finset (EuclideanSpace ℝ (Fin 2))), balanced S ∧ S.card = n) ∧
    {n | n ≥ 3 ∧ (∃ (S : Finset (EuclideanSpace ℝ (Fin 2))), balanced S ∧ centre_free S ∧ S.card = n)} =
    (({n | n ≥ 3 ∧ Odd n}) : Set ℕ ) := by sorry
Problem: The sequence $a_1,a_2,\dots$ of integers satisfies the conditions: (i) $1\le a_j\le2015$ for all $j\ge1$, (ii) $k+a_k\neq \ell+a_\ell$ for all $1\le k<\ell$. Prove that there exist two positive integers $b$ and $N$ for which\[\left\vert\sum_{j=m+1}^n(a_j-b)\right\vert\le1007^2\]for all integers $m$ and $n$ such that $n>m\ge N$.

Lean formal statement:
import Mathlib

theorem imo_2015_p6 (a : ℕ+ → ℤ) (ha1 : ∀ j : ℕ+, 1 ≤ a j ∧ a j ≤ 2015)
    (ha2 : ∀ k l, k < l → k + a k ≠ l + a l) :
    ∃ b N : ℕ+, ∀ m n, n > m ∧ m ≥ N → |(∑ j ∈ Finset.Icc (m + 1) n, (a j - b))| ≤ 1007^2 := by sorry
Problem: Find all integers $n$ for which each cell of $n \times n$ table can be filled with one of the letters $I,M$ and $O$ in such a way that: in each row and each column, one third of the entries are $I$, one third are $M$ and one third are $O$; and in any diagonal, if the number of entries on the diagonal is a multiple of three, then one third of the entries are $I$, one third are $M$ and one third are $O$. Note. The rows and columns of an $n \times n$ table are each labelled $1$ to $n$ in a natural order. Thus each cell corresponds to a pair of positive integer $(i,j)$ with $1 \le i,j \le n$. For $n>1$, the table has $4n-2$ diagonals of two types. A diagonal of first type consists all cells $(i,j)$ for which $i+j$ is a constant, and the diagonal of this second type consists all cells $(i,j)$ for which $i-j$ is constant.
Answer: {n | 9 ∣ n}

Lean formal statement:
import Mathlib

open Finset

inductive Letters
  | I | M | O
deriving BEq, DecidableEq

def diagonal_I_set (n k : ℕ) : Finset (Fin n × Fin n) :=
  (@Finset.univ (Fin n × Fin n) _ |>.filter (fun (i, j) => i.1 + j.1 = k))

def diagonal_I (n k : ℕ) (A : Matrix (Fin n) (Fin n) Letters) : Prop :=
  3 ∣ #(diagonal_I_set n k) →
  #(diagonal_I_set n k) = 3 * #{x ∈ diagonal_I_set n k | A x.1 x.2 = Letters.I} ∧
  #(diagonal_I_set n k) = 3 * #{x ∈ diagonal_I_set n k | A x.1 x.2 = Letters.M} ∧
  #(diagonal_I_set n k) = 3 * #{x ∈ diagonal_I_set n k | A x.1 x.2 = Letters.O}

def diagonal_II_set (n : ℕ) (k : ℤ) : Finset (Fin n × Fin n) :=
  (@Finset.univ (Fin n × Fin n) _ |>.filter (fun (i, j) => (i.1 : ℤ) - (j.1 : ℤ) = k))

def diagonal_II (n : ℕ) (k : ℤ) (A : Matrix (Fin n) (Fin n) Letters) : Prop :=
  3 ∣ #(diagonal_II_set n k) →
  #(diagonal_II_set n k) = 3 * #{x ∈ diagonal_II_set n k | A x.1 x.2 = Letters.I} ∧
  #(diagonal_II_set n k) = 3 * #{x ∈ diagonal_II_set n k | A x.1 x.2 = Letters.M} ∧
  #(diagonal_II_set n k) = 3 * #{x ∈ diagonal_II_set n k | A x.1 x.2 = Letters.O}

def exists_valid_table (n : ℕ) : Prop :=
  ∃ (A : Matrix (Fin n) (Fin n) Letters),
  (∀ i : Fin n,
    n = 3 * #{j | A i j = Letters.I} ∧ n = 3 * #{j | A i j = Letters.M} ∧
    n = 3 * #{j | A i j = Letters.O}) ∧
  (∀ j : Fin n,
    n = 3 * #{i | A i j = Letters.I} ∧ n = 3 * #{i | A i j = Letters.M} ∧
    n = 3 * #{i | A i j = Letters.O}) ∧
  (∀ k ∈ Finset.range (2 * n - 1), diagonal_I n k A) ∧
  ∀ k ∈ Finset.Icc (-(n : ℤ) + 1) (n - 1), diagonal_II n k A

theorem imo_2016_p2 : {n | exists_valid_table n} = (({n | 9 ∣ n}) : Set ℕ ) := by sorry