Sendov's Conjecture

Let $p$ be a complex polynomial of degree $n \ge 2$ whose zeros all lie in the closed unit disk. Then for every zero $a$ of $p$, there exists a critical point $\zeta$ of $p$ such that $|\zeta-a| \le 1$. This is the standard Sendov statement and exactly matches the theorem Mazur formalized.

Sendov's conjecture is resolved for every degree n >= 2, closing a gap that had stood since 1959: degrees up to eight were settled piecemeal between 1969 and 1999, and Tao's 2020 result covered all sufficiently large degrees without ever specifying the threshold, leaving the middle range open. Tao's digestion establishes the stronger interior form of the statement, which resolves the Phelps-Rodriguez conjecture in full generality as a consequence - a second conjecture falling out of the same argument, and one that likely merits its own entry. Two independent Lean developments now exist: Mazur's original at roughly 90,000 lines and Tao's streamlined version at about 15,000.