Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1985P2

module

public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Analysis.Normed.Order.Lattice
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1985, Problem 2

Find all real roots of the quartic x⁴ - (2N + 1)x² - x + N² + N - 1 = 0
correct to 4 decimal places, where N = 10¹⁰.
-/

namespace Usa1985P2

/-- The two real roots, correct to 4 decimal places. -/
/- determine -/ abbrev answer : ℝ × ℝ := sorry

theorem usa1985_p2 (N : ℝ) (hN : N = 10 ^ 10) :
    ∃ x₁ x₂ : ℝ, x₁ < x₂ ∧
      (∀ x : ℝ, x ^ 4 - (2 * N + 1) * x ^ 2 - x + N ^ 2 + N - 1 = 0 ↔
        x = x₁ ∨ x = x₂) ∧
      |x₁ - answer.1| < 0.00005 ∧ |x₂ - answer.2| < 0.00005 := sorry

end Usa1985P2

File author(s): Kimi K3

This problem has a complete formalized solution.