Sendov's conjecture finally proved for all degrees
A digestion of the proof of Sendov's conjecture
Terry Tao presents a human-readable digestion of an AI-generated proof that resolves Sendov's conjecture for every polynomial degree, along with the stronger Phelps–Rodriguez conjecture. The argument is remarkably elementary, relying only on the fundamental theorem of algebra, Möbius transformations, and a special case of Maclaurin's inequality. A Lean formalization with about 15,000 lines of code verifies the proof, which also yields a new proof of Rubinstein's theorem.
The proof ends up being remarkably elementary. No complex analysis is used other than the fundamental theorem of algebra (and very basic facts about Möbius transformations); and the deepest inequality used as input is the Maclaurin inequality.