Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2026P3

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.AlgebraicTopology.SimplexCategory.Basic
public import Mathlib.Data.List.GetD
public import Mathlib.RingTheory.PicardGroup

public section


/-!
# International Mathematical Olympiad 2026, Problem 3

Let n be a positive integer. Liu Bang and Xiang Yu have a stick of length 1
and want to divide it between themselves. Liu marks at most n points on the
stick, and then Xiang marks at most n points on the stick. The marked points
are distinct. Then, the stick is cut at all marked points, creating a number
of pieces. Afterwards, they take turns claiming any unclaimed piece of the
stick, with Liu going first. Each player's goal is to maximise the total
length of their own pieces.

For each n, determine the largest value c such that Liu may guarantee a total
length of at least c, regardless of Xiang's play.
-/

namespace Imo2026P3

noncomputable section

open scoped BigOperators

/-- The multiset of piece lengths obtained by cutting `[0,1]` at the points of a
finite set `S ⊆ (0,1)`.  We sort `S` ascending, prepend `0` and append `1`, and
take consecutive differences.  The result is a list of `|S| + 1` positive reals
summing to `1` (when `S ⊆ (0,1)`). -/
def pieceLengths (S : Finset ℝ) : List ℝ :=
  let l : List ℝ := (0 : ℝ) :: (S.sort (· ≤ ·)) ++ [1]
  List.zipWith (fun a b => b - a) l l.tail

/-- The sum of the entries of a list `L` at the (0-indexed) even positions, after
sorting `L` in non-increasing order.  These are the entries in the `1`st, `3`rd,
`5`th, … positions of the sorted (decreasing) list, i.e. the pieces claimed by
the first mover under the greedy claiming rule. -/
def firstPlayerShare (L : List ℝ) : ℝ :=
  let sorted := L.mergeSort (· ≥ ·)
  ((sorted.zipIdx.filter (fun p => p.2 % 2 = 0)).map (fun p => p.1)).sum

/-- `L(A,B)`: Liu Bang's total length, given Liu Bang's marks `A` and Xiang Yu's
marks `B`. -/
def L (A B : Finset ℝ) : ℝ :=
  firstPlayerShare (pieceLengths (A ∪ B))

/-- The set of admissible markings for a player: a finite subset of `(0,1)` of
size at most `n`.  We encode it as a `Finset ℝ` subject to the side conditions. -/
def AdmissibleMark (n : ℕ) (X : Finset ℝ) : Prop :=
  (↑X ⊆ Set.Ioo (0 : ℝ) 1) ∧ X.card ≤ n

/-- The value Liu Bang can guarantee.

`V n` is the supremum over Liu Bang's admissible markings `A` of the infimum,
over Xiang Yu's admissible markings `B` disjoint from `A`, of `L A B`. -/
def V (n : ℕ) : ℝ :=
  ⨆ A : {A : Finset ℝ // AdmissibleMark n A},
    ⨅ B : {B : Finset ℝ // AdmissibleMark n B ∧ Disjoint A.1 B}, L A.1 B.1
/- determine -/ abbrev answer (n : ℕ) : ℝ := sorry

end

theorem imo2026_p3 (n : ℕ) (hn : 0 < n) : V n = answer n := sorry

end Imo2026P3

File author(s): Kimi K3

This problem has a complete formalized solution.

The problem was imported from https://github.com/humanfia/imo2026.