Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2023P5

module

public import Mathlib.Algebra.BigOperators.Intervals
public import Mathlib.Algebra.Order.BigOperators.Group.Finset
public import Mathlib.Data.Nat.Log
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring

public section


/-!
# International Mathematical Olympiad 2023, Problem 5

Let n be a positive integer. A _Japanese triangle_ is defined as
a set of 1 + 2 + ... + n dots arranged as an equilateral
triangle. Each dot is colored white or red, such that each row
has exactly one red dot.

A _ninja path_ is a sequence of n dots obtained by starting in the
top row (which has length 1), and then at each step going to one of
the dot immediately below the current dot, until the bottom
row is reached.

In terms of n, determine the greatest k such that in each Japanese triangle
there is a ninja path containing at least k red dots.

The lower-bound argument formalized here follows Helio Ng's proof.
-/

namespace Imo2023P5

structure JapaneseTriangle (n : ℕ) where
  red : (i : Finset.Icc 1 n) → Fin i.val

def next_row {n} (i : Finset.Icc 1 n) (h : i.val + 1 ≤ n) : Finset.Icc 1 n :=
  ⟨i.val + 1, by aesop⟩

structure NinjaPath (n : ℕ) where
  steps : (i : Finset.Icc 1 n) → Fin i.val
  steps_valid : ∀ i : Finset.Icc 1 n, (h : i.val + 1 ≤ n) →
     ((steps i).val = steps (next_row i h) ∨
      (steps i).val + 1 = steps (next_row i h))

/- determine -/ abbrev solution_value (n : ℕ) : ℕ := sorry

theorem imo2023_p5 (n : ℕ) :
    IsGreatest {k | ∀ j : JapaneseTriangle n,
                    ∃ p : NinjaPath n,
                      k ≤ Fintype.card {i // j.red i = p.steps i}}
               (solution_value n) := sorry

end Imo2023P5

File author(s): David Renshaw, Kimi K3

This problem has a complete formalized solution.