Compfiles/Imo2026P6.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

2 declarations, 0 contain sorry, 0 declared as axioms

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).

Imports (2)
Imported by 1 file
  1. def Imo2026P6.IsValidSeq Documented declaration: IsValidSeq line 42 source

    Source documentation

    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.

    no axioms what this means

    Statement uses: Nat

    Proof uses: And, LT.lt, OfNat.ofNat, HAdd.hAdd, LE.le, Nat.gcd, Exists, Eq

    5 instances, coercions and auxiliary constants left out.

    def IsValidSeq (a : ℕ → ℕ) : Prop :=
…
  2. problem Imo2026P6.imo2026_p6 For any sequence satisfying Definition 1, there exist positive integers T and L such that a (n + T) = a n + L for every n line 50 source

    Source documentation

    For any sequence satisfying Definition 1, there exist positive integers T and L such that a (n + T) = a n + L for every n.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Imo2026P6.IsValidSeq, Exists, And, LT.lt, OfNat.ofNat, Eq, HAdd.hAdd

    Proof uses: Nat.gcd, LE.le, HSub.hSub, And.left, And.right, Eq.mp, congrArg, Nat.sub_add_cancel, StrictMono, strictMono_nat_of_lt_succ, Nat.recAux, of_eq_true, Eq.trans, True, congrFun', add_zero, And.intro, Or, lt_trichotomy, Eq.mpr and 121 more

    135 instances, coercions and auxiliary constants left out.

    Tactic trace: 503 steps (first 200 of 503)

    Open to load the checked before-and-after goal states.

    problem imo2026_p6 (a : ℕ → ℕ) (ha : IsValidSeq a) :
    ∃ T L : ℕ, 0 < T ∧ 0 < L ∧ ∀ n, a (n + T) = a n + L := by
…

    Mentions: Imo2026P6.IsValidSeq