smale_17_points_problem
Provedcomputational-complexity
Smale's 17th problem (1998): Can the eigenvalues of a symmetric matrix be computed with polynomial cost (in the BSS model over ℝ)? More generally, Smale's 7th problem asks for efficient algorithms for systems of polynomial equations over ℝ. Open for many formulations.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem smale_17_points_problem :
∃ (algo : (ℕ → ℕ → ℝ) → ℕ → Option (ℕ → ℝ)),
∀ (n : ℕ) (coeffs : ℕ → ℕ → ℝ),
(∃ x : ℕ → ℝ, ∀ i < n, ∑ j ∈ Finset.range n, coeffs i j * x j = 0) →
∃ T : ℕ, (algo coeffs T).isSome ∧
∀ sol, algo coeffs T = some sol →
∀ i < n, ∑ j ∈ Finset.range n, coeffs i j * sol j = 0 := by
sorrySource