Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1977P1

import Mathlib.Data.PNat.Basic
import Mathlib.Algebra.Polynomial.Basic

/-!
# USA Mathematical Olympiad 1977, Problem 1

Determine all pairs of positive integers (m, n) such that

  1 + x ^ n + x ^ (2 * n) + ... + x ^ (m * n)

is divisible by

  1 + x + x ^ 2 + ... + x ^ m.
-/

namespace Usa1977P1

open Polynomial

noncomputable def geomSumStep (m n : ℕ+) : ℤ[X] :=
  ∑ k ∈ Finset.range (m + 1), X ^ (k * n : ℕ)

noncomputable def geomSum (m : ℕ+) : ℤ[X] :=
  ∑ k ∈ Finset.range (m + 1), X ^ k

/- determine -/ abbrev solution_set : Set (ℕ+ × ℕ+) := sorry

theorem usa1977_p1 (m n : ℕ+) :
    (m, n) ∈ solution_set ↔ geomSum m ∣ geomSumStep m n := sorry

end Usa1977P1

File author(s): Karl Mehltretter

This problem does not yet have a complete formalized solution.