Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1992P6

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1992, Problem 6

For each positive integer $n$, $S(n)$ is defined to be the greatest integer such that, for every positive integer $k \le S(n)$, $n^{2}$ can be written as the sum of $k$ positive squares.

(a) Prove that $S(n) \le n^{2}-14$ for each $n \ge 4$.

(b) Find an integer $n$ such that $S(n)=n^{2}-14$.

(c) Prove that there are infinitely many integers $n$ such that $S(n)=n^{2}-14$.
-/

namespace Imo1992P6

/--
$z$ can be written as the sum of $k$ positive squares.
-/
def is_sum_of_pos_squares (z k : ℕ) : Prop := ∃ s : (Fin k → ℕ), z = ∑ i, (s i)^2 ∧ ∀ i, 0 < s i


/--
Auxiliary definition: S(n) will be defined as the greatest integer of the set S_set(n).
-/
def S_set (n : ℕ+) := { z : ℕ+ | ∀ k, k ≤ z → is_sum_of_pos_squares (n^2) k }

/-!
The definition of $S(n)$ in the problem statement hides a lot of complexity. The following lemmas are needed to write down $S(n)$ in a well-defined way.
-/

lemma S_set_Nonempty (n : ℕ+) : Set.Nonempty (S_set n) := by
  apply Set.nonempty_of_mem (x:=1)
  simp_rw [S_set, is_sum_of_pos_squares]
  intro k kle1
  use λi => n
  simp_all

lemma S_set_bounded (n) : ∀ k ∈ S_set n, k ≤ n^2 := by
  simp_rw [S_set, is_sum_of_pos_squares, Set.mem_setOf_eq]
  intro k kh
  let kh := kh k
  simp only [le_refl, forall_const] at kh
  let ⟨s,sh1, sh2⟩ := kh
  rw [←PNat.coe_le_coe]
  norm_cast at sh1
  rw [sh1]
  calc
    _ = ∑ i : Fin k, 1 := by simp
    _ ≤ _ := by
      apply Finset.sum_le_sum
      intro i _
      exact Nat.one_le_pow 2 (s i) (sh2 i)

lemma S_set_Finite (n) : Set.Finite (S_set n) := by
  apply Set.Finite.of_finite_image (f:=Subtype.val)
  · refine Set.finite_iff_bddAbove.mpr ?_
    refine bddAbove_def.mpr ?_
    use n^2
    simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right,
      forall_exists_index]
    intro y ypos h
    norm_cast
    let := (S_set_bounded n ⟨y, ypos⟩) h
    simp_all only [PNat.pow_coe, ge_iff_le]
    exact this
  · simp

noncomputable def S (n : ℕ+) := (Set.Finite.exists_maximal (S_set_Finite n) (S_set_Nonempty n)).choose


/- determine -/ abbrev imo1992_p6_b : ℕ+ := sorry

theorem imo1992_p6 : (∀ n ≥ 4, S n ≤ n^2-14) ∧ (S imo1992_p6_b = imo1992_p6_b^2 - 14) ∧ ({n | S n = n^2 - 14}.Infinite) := sorry


end Imo1992P6

File author(s): Constantin Seebach

This problem has a complete formalized solution.