AI-Generated and Lean-Checked Proof Resolves Sendov's Conjecture
Lech Mazur presents a computer-assisted proof of Sendov's conjecture developed substantially with OpenAI GPT-5.6 Pro and accompanied by a separate Lean 4 formalization; Terence Tao subsequently digested and streamlined the argument with further AI assistance, while noting that specialist review of the exposition and its relation to the formal development remains welcome.
On August 5, 2026, Lech Mazur presented a computer-assisted proof of Sendov's conjecture, with a separate Lean 4 formalization of the theorem. The conjecture states that if all zeros of a complex polynomial lie in the closed unit disk, then every zero lies within distance one of a critical point. Mazur's proof also yields the stronger interior statement used to derive the Phelps-Rodriguez conjecture.
Mazur discloses that OpenAI GPT-5.6 Pro played a substantial role in mathematical exploration, proof development, exact computation, adversarial auditing, and exposition, while he designed the workflow, selected and reconciled outputs, and takes responsibility for the manuscript. In an August 12 exposition, Terence Tao reports using heavy assistance from additional, unspecified AI agents to digest, contextualize, simplify, and streamline the proof. Tao's account extracts an elementary argument based on four identities relating zeros and critical points, Maclaurin-type inequalities, and a finite exact check for the remaining degrees.
The Lean development proves the exact theorem but is not a line-by-line verification of Mazur's manuscript or its supplementary certificate programs. Tao reports producing a shorter, approximately 15,000-line Lean formalization of the digested argument, compared with roughly 90,000 lines in the original development; both the correspondence between exposition and formal proof and the broader priority claims remain open to specialist review.