Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2026P6

module

public import Mathlib.Data.Nat.Squarefree

public section


/-!
# International Mathematical Olympiad 2026, Problem 6

Let a₁, a₂, a₃, … be an infinite sequence of positive integers greater
than 1. Suppose that for all positive integers n, the number a_{n+1} is the
smallest positive integer greater than a_n such that gcd(a_{n+1}, a_i) > 1
for every i = 1, 2, …, n.

Prove that there exist positive integers T and L such that a_{n+T} = a_n + L
for every positive integer n.

(Note that gcd(x, y) denotes the greatest common divisor of positive integers
x and y.)

Statement formalization adapted from AxiomMath/IMO2026; proof adapted from Humanfia's Kimi-K3 solutions (https://github.com/humanfia/imo2026).
-/

namespace Imo2026P6

/-- The predicate stating that `a : ℕ → ℕ` (0-indexed) is a sequence satisfying Definition 1:
each term exceeds `1`, and each subsequent term is the smallest integer strictly larger than the
previous one that shares a common factor with every earlier term. -/
def IsValidSeq (a : ℕ → ℕ) : Prop :=
  (∀ n, 1 < a n) ∧
  (∀ n, a n < a (n + 1) ∧
        (∀ i ≤ n, 1 < Nat.gcd (a (n + 1)) (a i)) ∧
        (∀ b, a n < b → b < a (n + 1) → ∃ i ≤ n, Nat.gcd b (a i) = 1))

/-- For any sequence satisfying Definition 1, there exist positive integers `T` and `L` such that
`a (n + T) = a n + L` for every `n`. Equivalently, the sequence of consecutive differences is
purely periodic. -/
theorem imo2026_p6 (a : ℕ → ℕ) (ha : IsValidSeq a) :
    ∃ T L : ℕ, 0 < T ∧ 0 < L ∧ ∀ n, a (n + T) = a n + L := sorry

end Imo2026P6

File author(s): Kimi K3

This problem has a complete formalized solution.

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