{"id":"palomar/PALOMAR-2026-08-20-000002","url":"https://github.com/yuanchenyang/lean_low_rank_univariate_sos/tree/1fccd921a4530a088ab6e230f832041ab3c5c7f3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000002-v1.json","repo":"https://github.com/yuanchenyang/lean_low_rank_univariate_sos","tags":["math.OC","math.AG","msc:90C23","msc:90C26","msc:90C22","msc:12D15","sum-of-squares","nonconvex-optimization","lean-formalization"],"score":0,"title":"yuanchenyang/lean_low_rank_univariate_sos","trust":"high","domain":"math.OC","source":"palomar","authors":["Chenyang Yuan"],"reviews":0,"subject":"math.OC","summary":"A Lean 4 formalization of the main theorem of Legat, Yuan and Parrilo, \"Low-Rank Univariate Sum of Squares Has No Spurious Local Minima\" (SIAM J. Optim. 33(3), 2023). For a real univariate polynomial p and a pair of polynomials u = (u₁, u₂), consider the quadratically penalized Burer–Monteiro objective f_p(u) = ‖σ(u) - p‖² with σ(u) = u₁² + u₂², the norm coming from any inner product on ℝ[x]. The formalized theorem states that if p is a sum of two squares (which is the case for any nonnegative univariate polynomial) and u is a second-order critical point of f_p (vanishing gradient and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"Low-Rank Univariate Sum of Squares Has No Spurious Local Minima","identifier":"doi:10.1137/22M1516208","relationship":"formalizes"}]}