A sum of squares tactic
I've put together an sos tactic: a sum-of-squares decision procedure for nonlinear real arithmetic, closely following John Harrison's implementation in HOL Light. It closes a range of polynomial-inequality goals over the reals that we don't otherwise have good tactics for.
Every example below is elaborated by Lean when this page is built — the tactic really runs, CSDP and all.
What it does
The idea is old and lovely: to show a polynomial is nonnegative, write it as a sum of squares. Finding that decomposition is a semidefinite program, and once you have it, the certificate is checkable by hand. Here's Cauchy–Schwarz, degree 4 in 4 variables:
example (a b c d : ℝ) :
0 ≤ (a^2 + b^2) * (c^2 + d^2) - (a*c + b*d)^2 := a:ℝb:ℝc:ℝd:ℝ⊢ 0 ≤ (a ^ 2 + b ^ 2) * (c ^ 2 + d ^ 2) - (a * c + b * d) ^ 2 All goals completed! 🐙Cyclic Schur in three variables:
example (a b c : ℝ) : 0 ≤ a^2 + b^2 + c^2 - a*b - b*c - a*c := a:ℝb:ℝc:ℝ⊢ 0 ≤ a ^ 2 + b ^ 2 + c ^ 2 - a * b - b * c - a * c All goals completed! 🐙Strict inequalities are fine too:
example (x y : ℝ) : 0 < x^2 + y^2 + 1 := x:ℝy:ℝ⊢ 0 < x ^ 2 + y ^ 2 + 1 All goals completed! 🐙
Hypotheses become constraints. With an equality constraint, the search finds the cofactor it needs — here -4a, giving the discriminant of a real-rooted quadratic:
example (a b c x : ℝ) (_h : a*x^2 + b*x + c = 0) :
0 ≤ b^2 - 4*a*c := a:ℝb:ℝc:ℝx:ℝ_h:a * x ^ 2 + b * x + c = 0⊢ 0 ≤ b ^ 2 - 4 * a * c All goals completed! 🐙
And with a few tricks it reaches beyond the reals. A goal over Nat gets negated and refuted over Real:
example : ∀ n : ℕ, n ≤ n * n := ⊢ ∀ (n : ℕ), n ≤ n * n All goals completed! 🐙How it works
End to end: reify the goal, encode a semidefinite program, call CSDP, round the floating-point Gram matrix back to rationals, decompose it via LDLᵀ plus Lagrange's four-square identity, and dispatch the matching verifier-soundness lemma. The rounding regime — try small integers first, then some powers of two — is lifted straight from Harrison's HOL Light code. I tried some variations, but none of them were justified by the test suite, so I reverted to copying Harrison exactly.
What it is not (yet)
Treat this as a prototype. It's not ready to become Mathlib PRs, let alone a grind plugin, because:
-
It depends on
csdp-ffi, an FFI wrapper around the CSDP library. We'd need to decide whether that's a Mathlib dependency or a runtime-only one (with Mathlib committing only witnesses produced bysos?). -
It depends on a computable multivariable-polynomial library,
CompPoly, which itself depends on Mathlib. -
The code still needs cleanup and review.
None of that changes what it can prove today, which is already more than I expected when I started.
Getting started
[[require]] name = "sos" git = "https://github.com/leanprover/sos" rev = "main"
Then import SOS and use by sos. You'll need the system BLAS/LAPACK runtime installed; see the README for the full showcase and native-dependency notes. There's also sos?, which prints the certificate it found so you can commit the witness directly instead of re-running the solver.