Researcher Simplifies AI-Generated Proof of Sendov’s Conjecture

Researchers have successfully resolved two longstanding mathematical conjectures regarding polynomial zeros and critical points, marking a significant advancement in the integration of artificial intelligence and formal verification in pure mathematics. The breakthrough addresses Sendov’s conjecture and its extension, the Phelps–Rodriguez conjecture, both of which propose that for any polynomial with roots confined to the unit disk, every root is accompanied by a critical point within a unit distance. The proof originated from an AI-generated argument developed by mathematician Lech Mazur. While the initial formal verification in the Lean theorem prover required approximately 90,000 lines of code, subsequent human-led analysis streamlined and digested the work into a more accessible, elementary framework. The refined approach relies primarily on the fundamental theorem of algebra, basic Möbius transformations, and the Maclaurin inequality. By establishing key geometric identities, specifically relating polynomial centroids, polar inversions, and origin constraints, the authors derived complementary polar and origin inequalities. These mathematical relationships create a contradiction when assuming the existence of a counterexample, thereby validating the conjectures for all polynomial degrees. The finalized proof has been rigorously formalized in Lean, reducing the verification code to roughly 15,000 lines. This dramatic compression demonstrates how human mathematical intuition can effectively distill and verify complex AI-generated outputs. The methodology not only confirms the conjectures but also yields a novel proof of Rubinstein’s theorem, which covers intermediate polynomial degrees. This achievement underscores a maturing paradigm in computational mathematics, where AI systems handle exploratory proof generation, while human experts refine logical structures and ensure formal rigor. The resolved conjectures share structural similarities with several open problems in geometric function theory, including Borcea’s, Schmeisser’s, and Smale’s conjectures. Although the current elementary techniques do not directly extend to these variants due to relaxed boundary constraints, the foundational identities and inequality frameworks established here provide a tested blueprint for future investigations. Recent automated search tools have also been deployed in parallel efforts to probe related conjectures without identifying counterexamples, further highlighting the collaborative potential of algorithmic exploration and formal proof. The successful resolution of Sendov’s and Phelps–Rodriguez’s conjectures stands as a benchmark for human-AI mathematical synergy, offering both a complete solution to a decades-old problem and a validated workflow for tackling other unresolved conjectures in complex analysis and algebra.