Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1988P5

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Polynomial.Eval.Coeff
public import Mathlib.Data.Rat.Star

public section


/-!
# USA Mathematical Olympiad 1988, Problem 5

Let p(x) be the polynomial (1 - x)ᵃ (1 - x²)ᵇ (1 - x³)ᶜ ... (1 - x³²)ᵏ,
where a, b, ..., k are integers. When expanded in powers of x, the coefficient
of x¹ is -2 and the coefficients of x², x³, ... , x³² are all zero. Find k.
-/

namespace Usa1988P5

open Polynomial

/-- The polynomial `p(x) = ∏_{i = 1}^{32} (1 - X^i) ^ (a i)`. The exponent
`a 32` of the last factor is the `k` of the problem. (We take the exponents
to be natural numbers; the coefficient conditions force every exponent to be
positive anyway.) -/
noncomputable def prodForm (a : ℕ → ℕ) : ℚ[X] := ∏ i ∈ Finset.Icc 1 32, (1 - X ^ i) ^ a i

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

theorem usa1988_p5 (a : ℕ → ℕ)
    (h1 : (prodForm a).coeff 1 = -2)
    (hz : ∀ k, 2 ≤ k → k ≤ 32 → (prodForm a).coeff k = 0) :
    a 32 = answer := sorry

end Usa1988P5

File author(s): Kimi K3

This problem has a complete formalized solution.