Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2008P1


import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2008, Problem 1

Prove that for each positive integer n, there are pairwise relatively prime
integers k₀,k₁,...,kₙ, all strictly greater than 1, such that k₀k₁...kₙ - 1
is a product of two consecutive integers.
-/

namespace Usa2008P1

open scoped BigOperators

theorem usa2008_p1 (n : ℕ) (hn : 0 < n) :
    ∃ k : Fin (n + 1) → ℕ,
      (∀ i, 1 < k i) ∧
      (∀ i j, i ≠ j → Nat.Coprime (k i) (k j)) ∧
      ∃ m, ∏ i : Fin (n + 1), k i = 1 + m * (m + 1) := sorry

This problem does not yet have a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org:
External resources: