Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1967P3

import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1967, Problem 3

Let $k, m, n$ be natural numbers such that m + k + 1 is a prime greater
than n + 1. Let c(s) = s * (s+1). Prove that the product
(c(m+1) - c(k)) * (c(m+2) - c(k)) * ... * (c(m+n) - c(k)) is divisible
by the product c(1) * c(2) * ... * c(n).
-/

namespace Imo1967P3



theorem imo1967_p3
  (k m n : ℕ)
  (c : ℕ → ℕ)
  (h₀ : 0 < k ∧ 0 < m ∧ 0 < n)
  (h₁ : ∀ s, c s = s * (s + 1))
  (h₂ : Nat.Prime (k + m + 1))
  (h₃ : n + 1 < k + m + 1) :
  (∏ i ∈ Finset.Icc 1 n, (↑(c i):ℤ)) ∣ (∏ i ∈ Finset.Icc 1 n, (((c (m + i)):ℤ) - ((c k):ℤ))) := sorry

File author(s): Roozbeh Yousefzadeh

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/Lean_v20/imo_proofs/imo_1967_p3.lean.