Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1984P1

module

public import Mathlib.Algebra.Polynomial.RingDivision
public import Mathlib.Analysis.CStarAlgebra.Classes
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1984, Problem 1

Two roots of the real quartic x⁴ - 18x³ + ax² + 200x - 1984 = 0
have product -32. Find a.
-/

namespace Usa1984P1

open Polynomial

/- determine -/ abbrev solution : ℝ := sorry

theorem usa1984_p1 (a : ℝ) (P : ℝ[X])
    (hP : P = X ^ 4 - 18 * X ^ 3 + C a * X ^ 2 + 200 * X - 1984)
    (x₁ x₂ : ℂ) (hx : x₁ ≠ x₂)
    (h₁ : aeval x₁ P = 0) (h₂ : aeval x₂ P = 0) (hprod : x₁ * x₂ = -32) :
    a = solution := sorry

end Usa1984P1

File author(s): Kimi K3

This problem has a complete formalized solution.