Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2012P3

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Data.Int.Star
public import Mathlib.NumberTheory.Bertrand

public section


/-!
# USA Mathematical Olympiad 2012, Problem 3

Determine which integers n > 1 have the property that there exists an infinite
sequence a₁, a₂, a₃, ... of nonzero integers such that the equality

  aₖ + 2a₂ₖ + ⋯ + naₙₖ = 0

holds for every positive integer k.
-/

namespace Usa2012P3

/- determine -/ abbrev SolutionSet : Set ℕ := sorry

theorem usa2012_p3 (n : ℕ) (hn : 1 < n) :
    n ∈ SolutionSet ↔ ∃ a : ℕ → ℤ, (∀ i, 1 ≤ i → a i ≠ 0) ∧
      ∀ k, 1 ≤ k → ∑ j ∈ Finset.Icc 1 n, (j : ℤ) * a (j * k) = 0 := sorry

File author(s): Kimi K3

This problem has a complete formalized solution.