Tao's digestion of the proof of Sendov's conjecture

Lech Mazur has announced an AI-assisted, Lean-verified proof of the 67 years old conjecture of Sendov , one of the most famous open problems in complex analysis. The conjecture states that every zero of a polynomial whose zeros lie in the closed unit disk is within distance one of a critical point. It appears that the proof of this remarkably simple statement ended up using equally elementary tools. As Tao writes: 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