Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2002P5

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Int.ConditionallyCompleteOrder
public import Mathlib.Data.Int.Star
public import Mathlib.Order.ConditionallyCompleteLattice.Basic
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2002, Problem 5

Let a, b be integers greater than 2. Prove that there exists a positive
integer k and a finite sequence n₁, n₂, ..., nₖ of positive integers such
that n₁ = a, nₖ = b, and nᵢ + nᵢ₊₁ divides nᵢnᵢ₊₁ for each i (1 ≤ i < k).
-/

namespace Usa2002P5

theorem usa2002_p5 (a b : ℤ) (ha : 2 < a) (hb : 2 < b) :
    ∃ k : ℕ, ∃ n : ℕ → ℤ, n 0 = a ∧ n k = b ∧
      (∀ i, i ≤ k → 0 < n i) ∧ ∀ i, i < k → n i + n (i + 1) ∣ n i * n (i + 1) := sorry

end Usa2002P5

File author(s): Kimi K3

This problem has a complete formalized solution.