Phelps–Rodriguez Conjecture

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 by this site on 13 August 2026, which is what lifts this above the submitter's conservative Lean-checked classification. The gap the submitter correctly 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 >= 2 and p of natDegree n with every root in the closed unit disk and p(a) = 0, either there is a critical point with the norm of (zeta - a) strictly below 1, or the norm of a is 1 and p = C c * (X^n - C (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 >= 2 forces p to be nonzero, which the proof derives rather than assumes. All 80 first-party Lean files were then downloaded and audited with comments stripped: zero admit, zero axiom declarations, zero native_decide, and 124 decide calls, all kernel-reduced. The repository's only two sorry occurrences sit in Challenge.lean, which nothing imports - it is a deliberate statement-of-record that leaves both theorems open for a reader to check against - so they are outside the proof path. On the build, the repository's four GitHub Actions runs all report failure, which is misleading and worth stating plainly: reading the job steps shows the leanprover/lean-action build step completed successfully on the latest commit, and the failing step is docgen-action, documentation generation. That makes the kernel check third-party evidenced on GitHub's runners rather than resting on the author's machine. Not independently reviewed by another mathematician: the repository says so itself, and Tao is both the author of the digestion and the director of the formalization.

Sources

• PaperTao, A digestion of the proof of Sendov's conjecture (12 Aug 2026)
• Lean proofteorth/sendov - Lean formalization; Sendov.phelps_rodriguez in Sendov/Conjecture.lean
• Lean statementChallenge.lean - the statement of record, Mathlib-only, no definitions of its own
• Independent workMazur's original proof of Sendov's conjecture, the underlying argument
• OtherA digestion of the proof of Sendov’s conjecture