Phelps–Rodriguez Conjecture

Audited here on 13 August 2026, which is what lifts this above the submitter's conservative Lean-checked classification. The gap they identified was that nobody had checked the correspondence between Tao's formal statement and the historical conjecture, so that check was performed. Sendov.phelps_rodriguez in Sendov/Conjecture.lean reads: for $n \ge 2$ and $p$ of natDegree $n$ with every root in the closed unit disk and $p(a)=0$, either some critical point has $|\zeta - a| < 1$, or $|a| = 1$ and $p = c(X^n - a^n)$ for some nonzero $c$. That is exactly Phelps-Rodriguez, exceptional family included, with no weakening; and it is not vacuous, since natDegree $= n$ with $n \ge 2$ forces $p \ne 0$, which the proof derives rather than assumes. All 80 first-party files were audited with comments stripped: zero admit, zero axiom declarations, zero native_decide, and 124 decide calls, all kernel-reduced. The only two sorry occurrences sit in Challenge.lean, which nothing imports, so they are outside the proof path. On the build, all four GitHub Actions runs report failure, which is misleading: reading the job steps shows the leanprover/lean-action build succeeded on the latest commit, and the failing step is docgen-action, documentation generation. That makes the kernel check third-party evidenced rather than resting on the author's machine. Not independently reviewed by another mathematician: the repository says so, and Tao both wrote the digestion and directed the formalization.