Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1973P3

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1973, Problem 3

Let $a$ and $b$ be real numbers for which the equation $x^4 + ax^3 + bx^2 + ax + 1 = 0$ has at least one real solution. For all such pairs $(a, b)$, find the minimum value of $a^2 + b^2$.

-/

namespace Imo1973P3

noncomputable abbrev solution : ℝ := (4:ℝ)/5

theorem imo1973_p3
  (S : Set (ℝ × ℝ))
  (hS : S = {(a, b) | ∃ x : ℝ, x ^ 4 + a * x ^ 3 + b * x ^ 2 + a * x + 1 = 0}) :
  IsLeast { x.1 ^ 2 + x.2 ^ 2 | x ∈ S } solution := 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_1973_p3.lean.