Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1994P1

module

public import Mathlib.Algebra.BigOperators.Ring.Finset
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.Linarith
public import Mathlib.Tactic.NormNum.Ineq
public import Mathlib.Tactic.Ring
public import Mathlib.Tactic.Zify

public section


/-!
# USA Mathematical Olympiad 1994, Problem 1

a₁, a₂, a₃, ... are positive integers such that aₙ > aₙ₋₁ + 1.
Put bₙ = a₁ + a₂ + ... + aₙ. Show that there is always a square in the
range bₙ, bₙ+1, bₙ+2, ... , bₙ₊₁-1.
-/

namespace Usa1994P1

theorem usa1994_p1 (a : ℕ → ℕ) (ha : ∀ i, 0 < a i)
    (h : ∀ i, a i + 1 < a (i + 1)) (n : ℕ) (hn : 1 ≤ n) :
    ∃ m : ℕ, (∑ i ∈ Finset.range n, a i) ≤ m ^ 2 ∧
      m ^ 2 < ∑ i ∈ Finset.range (n + 1), a i := sorry

end Usa1994P1

File author(s): Kimi K3

This problem has a complete formalized solution.