module
public import Mathlib.Algebra.GCDMonoid.Multiset
public import Mathlib.Algebra.GCDMonoid.Nat
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Prod.Lex
public import Mathlib.NumberTheory.Padics.PadicVal.Basic
public section
/-!
# International Mathematical Olympiad 2026, Problem 1
There are 2026 integers greater than 1 written on a blackboard, not necessarily
different. In a move, Confucius chooses two integers m > 1 and n > 1 from
different places on the blackboard and replaces these two integers with
gcd(m, n) and lcm(m, n) / gcd(m, n). He continues to make moves while it is
possible to do so.
(a) Prove that, regardless of the choices of Confucius, after finitely many
moves, exactly one integer M on the blackboard is greater than 1.
(b) Prove that the value of M does not depend on the choices of Confucius.
(Note that gcd(x, y) denotes the greatest common divisor of positive integers
x and y, and lcm(x, y) denotes the least common multiple of x and y.)
Statement formalization adapted from AxiomMath/IMO2026; proof adapted from
Humanfia's Kimi-K3 solutions (https://github.com/humanfia/imo2026).
-/
namespace Imo2026P1
/-- A *board* is a finite multiset of natural numbers. The full board discipline
(entries `≥ 1`, cardinality `2026`) is captured by the predicate `IsInitial`. -/
abbrev Board := Multiset ℕ
/-- An *initial board*: exactly `2026` entries, each strictly greater than `1`. -/
def IsInitial (B : Board) : Prop :=
Multiset.card B = 2026 ∧ ∀ a ∈ B, 1 < a
/-- A single *move*: pick two entries `m, n` (from two distinct positions,
modelled as two separate elements of the multiset) both `> 1`, remove them and
insert `gcd(m, n)` and `lcm(m, n) / gcd(m, n)`. Using `m ::ₘ n ::ₘ s` for the
source board automatically encodes that the two chosen positions are distinct
(they are two separate multiset elements, whose *values* may coincide). -/
def Move (B B' : Board) : Prop :=
∃ (m n : ℕ) (s : Board), 1 < m ∧ 1 < n ∧
B = m ::ₘ n ::ₘ s ∧
B' = Nat.gcd m n ::ₘ (Nat.lcm m n / Nat.gcd m n) ::ₘ s
/-- A board is *terminal* when at most one entry is `> 1`, so no move is possible. -/
def IsTerminal (B : Board) : Prop :=
Multiset.card (B.filter (fun a => 1 < a)) ≤ 1
/-- A board has a *unique large entry* when exactly one entry is `> 1`. -/
def HasUniqueLarge (B : Board) : Prop :=
Multiset.card (B.filter (fun a => 1 < a)) = 1
/-- `Reachable B B'` : `B'` can be obtained from `B` by a finite sequence of moves
(the reflexive–transitive closure of `Move`). A finite play from `B` to a
terminal board `B'` is precisely a witness of `Reachable B B'` with `IsTerminal B'`. -/
def Reachable (B B' : Board) : Prop := Relation.ReflTransGen Move B B'
/-- The exponent `g_p` for a prime `p` and board `B`: the `gcd` of the `p`-adic
valuations of the entries of `B`. Since `gcd(a, 0) = a`, valuations equal to `0`
(entries not divisible by `p`) do not affect this gcd, so `gExp p B` is the gcd of
the *positive* `p`-adic valuations occurring in `B`. -/
noncomputable def gExp (p : ℕ) (B : Board) : ℕ :=
(B.map (fun a => padicValNat p a)).gcd
/-- The claimed invariant terminal value
`M = ∏_{p ∣ ∏ B} p ^ gExp p B`, the product over all primes dividing some entry
of `B` of `p` raised to the gcd of the `p`-adic valuations. -/
noncomputable def Mval (B : Board) : ℕ :=
∏ p ∈ B.prod.primeFactors, p ^ gExp p B
/-- **Statement (a), part 1 — termination.** There is no infinite play starting
from an initial board `B₀`: no infinite sequence of boards can start at `B₀` and
have every consecutive pair related by a `Move`. -/
theorem imo2026_p1a_termination (B₀ : Board) (hB₀ : IsInitial B₀) :
¬ ∃ f : ℕ → Board, f 0 = B₀ ∧ ∀ k, Move (f k) (f (k + 1)) := sorry
/-- **Statement (a), part 2 — unique large entry.** Any terminal board reachable
from an initial board `B₀` has exactly one entry `> 1`. -/
theorem imo2026_p1a_unique_large (B₀ : Board) (hB₀ : IsInitial B₀)
(B' : Board) (hreach : Reachable B₀ B') (hterm : IsTerminal B') :
HasUniqueLarge B' := sorry
/-- **Statement (b) — invariance of `M`.** Any two terminal boards reachable from
the same initial board `B₀` have the same set of entries `> 1`; since (by (a)) each
has exactly one such entry, this says the terminal value `M` is the same for both. -/
theorem imo2026_p1b_invariance (B₀ : Board) (hB₀ : IsInitial B₀)
(B₁ B₂ : Board) (h₁ : Reachable B₀ B₁) (h₂ : Reachable B₀ B₂)
(t₁ : IsTerminal B₁) (t₂ : IsTerminal B₂) :
∀ M, (1 < M ∧ M ∈ B₁) ↔ (1 < M ∧ M ∈ B₂) := sorry
/-- **Value of `M` (correctness of the explicit formula).** For any terminal board
`B'` reachable from an initial board `B₀`, the unique entry `M > 1` of `B'` equals
the invariant `Mval B₀`. -/
theorem imo2026_p1_terminal_value (B₀ : Board) (hB₀ : IsInitial B₀)
(B' : Board) (hreach : Reachable B₀ B') (hterm : IsTerminal B')
(M : ℕ) (hM : 1 < M) (hMem : M ∈ B') :
M = Mval B₀ := sorry
/-- The invariant terminal value is itself `> 1`, since all initial entries exceed
`1`. -/
theorem imo2026_p1_mval_gt_one (B₀ : Board) (hB₀ : IsInitial B₀) : 1 < Mval B₀ := sorry
end Imo2026P1
This problem has a complete formalized solution.
The problem was imported from https://github.com/humanfia/imo2026.