Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1989P1

import Mathlib.Tactic
import Mathlib.Tactic.NthRewrite
import Mathlib.Data.Rat.Defs
import Mathlib.Data.Fin.Basic

/-!
# USA Mathematical Olympiad 1989, Problem 1

For each positive integer n, let
  Sn = 1 + 1/2 + 1/3 + ··· + 1/n
  Tn = S1 + S2 + S3 + ··· + Sn
  Un = T1/2 + T2/3 + T3/4 + ··· + Tn/(n+1)
Find, with proof, integers 0 < a, b, c, d < 1000000 such that
  T1988 = a * S1989 - b
  U1988 = c * S1989 - d
-/

namespace Usa1989P1

def s (n : ℕ) : ℚ := ∑i ∈ Finset.Icc 1 n, 1 / i
def t (n : ℕ) : ℚ := ∑i ∈ Finset.Icc 1 n, s i
def u (n : ℕ) : ℚ := ∑i ∈ Finset.Icc 1 n, t i / (i + 1)

/- determine -/ abbrev solutions : (ℕ × ℕ × ℕ × ℕ) := sorry

theorem usa1989_p1 :
    t 1988 = solutions.1 * s 1989 - solutions.2.1 ∧
    u 1988 = solutions.2.2.1 * s 1989 - solutions.2.2.2 := sorry


end Usa1989P1

File author(s): Shalev Wengrowsky

This problem has a complete formalized solution.