Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1986P3

module

public import Mathlib.Algebra.GCDMonoid.Nat
public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Nat.Prime.Defs
public import Mathlib.Data.ZMod.Defs
public import Mathlib.RingTheory.Coprime.Lemmas
public import Mathlib.Tactic.IntervalCases
public import Mathlib.Tactic.LinearCombination

public section


/-!
# USA Mathematical Olympiad 1986, Problem 3

What is the smallest n > 1 for which the average of the first n
(non-zero) squares is a square?
-/

namespace Usa1986P3

/- determine -/ abbrev solution : ℕ := sorry

theorem usa1986_p3 :
    IsLeast {n : ℕ | 1 < n ∧ ∃ m, ∑ i ∈ Finset.range n, (i+1)^2 = n * m^2}
      solution := sorry

end Usa1986P3

File author(s): Kimi K3

This problem has a complete formalized solution.