The Phelps-Rodriguez conjecture (Phelps and Rodriguez 1972) is the strengthening of the Sendov conjecture asserting that for
a polynomial of polynomial degree
with all zeros in the closed
unit disk, every zero
has a critical point
satisfying
unless
and
is a nonzero scalar multiple of
.
In the exceptional case, all critical points equal 0 and their distance from is 1. Tao (2026) showed that the AI-generated proof of the
Sendov conjecture also establishes this stronger
statement, and supplied a Lean formalization.