Borcea's 2-variance conjecture asserts that for a complex polynomial of degree n≥2, every zero lies within distance σ2(P) of some critical point. Here σ2(P) is the standard deviation of the zeros.

A hypothetical counterexample is normalized so that the centroid is 0, the variance is 1 and the prescribed zero is a>0. The argument then uses Schoenberg's inequality, reciprocal-moment bounds and integral estimates on products. An analytic argument excludes degrees n≥100001. Product and coefficient bounds, together with a computer-assisted finite verification over a bounded parameter box, handle the remaining degrees. The main results are also formalized in Lean 4.

The paper proves Borcea's 2-variance conjecture for all degrees. A Lean 4 formalization of the main results accompanies the proof.