Phelps–Rodriguez Conjecture

Let $p$ be a complex polynomial of degree $n\ge2$ whose zeros all lie in the closed unit disk. For every zero $a$ of $p$ , there is a critical point $\zeta$ satisfying $|\zeta-a|<1$ , except when $|a|=1$ and $p$ is a nonzero scalar multiple of $z^n-a^n$ .

Result: Proved(see note)
Status: Resolved
AI contribution: AI co-developed
Method: Argument
Field: Complex analysis
Posed by: Dean Phelps, Rene S. Rodriguez
Year posed: 1972
Years open: 54y
Solved: 2026-08-12
Model: GPT-5.6 Pro, Claude Opus 5
Vendor: OpenAI
Collaborators: Lech Mazur, Terence Tao
Verification: Lean-verified
Publication: Announced
Significance: 30 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Phelps-Rodriguez implies Sendov, so this entry records the stronger of the pair; the companion Sendov entry records the weaker statement and Mazur's original formalization, which proved Sendov but never stated the equality classification. The exceptional family is genuinely attained rather than an artefact of the proof: for p = z^n - 1 and a = 1 the only critical point is the origin, at distance exactly 1. Both conjectures fell out of one argument, and the strict form was not the announced target - Tao's digestion of Mazur's proof turned out to establish it, which is how a 1972 conjecture was resolved as a by-product of resolving a 1959 one.

What the AI did

Two models in two roles. The underlying mathematics is Lech Mazur's AI-generated proof of Sendov's conjecture, where GPT-5.6 Pro carried the discovery and derivation. Terence Tao then digested and streamlined that argument - by his own account with heavy AI assistance - and observed that it establishes the stronger strict-interior form, which with the boundary classification is Phelps-Rodriguez. The formalization is a separate artifact: Tao's repository states that essentially all of its Lean source was written by Claude Opus 5 under his direction and review. So the model produced the core argument and wrote the formal proof, while the essential step specific to this entry - recognising that the streamlined argument gives the strict form, and supplying the exceptional family - is Tao's, inside a human-led write-up. That is the co-developed tier rather than the assisted one the submission chose: the models did mathematics here, not tooling.

Verification

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.

Sources

Related entries

Same work resolves bothSendov's Conj.

Submitted by HiddenHawk615 on 13 Aug 2026