Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1972P4

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Algebra.Order.Star.Real
public import Mathlib.Algebra.Ring.IsFormallyReal
public import Mathlib.Data.Int.Star
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.LinearCombination.Lemmas
public import Mathlib.Tactic.Linarith
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1972, Problem 4

Let k be the real cube root of 2. Find integers A, B, C, a, b, c such that

  |(Ax² + Bx + C)/(ax² + bx + c) − k| < |x − k|

for all non-negative rational numbers x.
-/

namespace Usa1972P4

/-- The property that the integers `A, B, C, a, b, c` solve the problem for the
real cube root `k` of `2`: the rational function `(Ax² + Bx + C)/(ax² + bx + c)`
approximates `k` strictly better than `x` does, for every non-negative
rational number `x`. -/
abbrev IsSolution (A B C a b c : ℤ) (k : ℝ) : Prop :=
  ∀ x : ℚ, 0 ≤ x →
    |((A : ℝ) * (x : ℝ) ^ 2 + (B : ℝ) * (x : ℝ) + (C : ℝ)) /
        ((a : ℝ) * (x : ℝ) ^ 2 + (b : ℝ) * (x : ℝ) + (c : ℝ)) - k| <
      |(x : ℝ) - k|

/- determine -/ abbrev solution : ℤ × ℤ × ℤ × ℤ × ℤ × ℤ := sorry

theorem usa1972_p4 (k : ℝ) (hk : k ^ 3 = 2) :
    match solution with
    | (A, B, C, a, b, c) => IsSolution A B C a b c k := sorry

end Usa1972P4

File author(s): Kimi K3

This problem has a complete formalized solution.