Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1977P2

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1977, Problem 2

In a finite sequence of real numbers the sum of any seven successive terms is negative and the sum of any eleven successive terms is positive.
Determine the maximum number of terms in the sequence.

-/

namespace Imo1977P2

def sum_successive_terms {α : Type} [AddCommMonoid α] {n : ℕ} (s : Fin n → α) (start : Fin n) (count : ℕ) [NeZero count] (h : start+count-1 < n) : α :=
  ∑ i ∈ Finset.Icc start ⟨start+count-1, h⟩, s i



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

theorem imo1977_p2 :
    Maximal (λn ↦ ∃ s : Fin n → ℝ, ∀ i0, (∀ h7, sum_successive_terms s i0 7 h7 < 0) ∧ (∀ h11, sum_successive_terms s i0 11 h11 > 0)) max_num_terms := sorry


end Imo1977P2

File author(s): Constantin Seebach

This problem has a complete formalized solution.