El matemático Terence Tao publica una versión depurada y legible de la demostración de la conjetura de Sendov obtenida en 2025 por Lech Mazur mediante una herramienta de inteligencia artificial, y cuya verificación formal en Lean ya estaba disponible. Tras varios días de trabajo asistido por IA, con apoyo adicional en papel y con otros agentes, Tao reorganiza el argumento, lo contextualiza con la literatura previa y lo simplifica para destacar las ideas principales. El resultado demuestra de hecho una versión más fuerte (la conjetura 3), lo que resuelve simultáneamente la conjetura de Sendov y su refuerzo de Phelps–Rodríguez en toda su generalidad, y ofrece además una nueva demostración del teorema de Rubinstein.
Sorprendentemente, la prueba es elemental: no utiliza análisis complejo más allá del teorema fundamental del álgebra y nociones básicas de transformaciones de Möbius, y la única desigualdad profunda que requiere es un caso particular de la desigualdad de Maclaurin, derivable a su vez de la desigualdad entre la media aritmética y la media armónica mediante un argumento inductivo. Usando de nuevo un agente de IA, Tao ha formalizado todo el argumento en Lean (unos 15.000 líneas de código, frente a las 90.000 de la formalización original) y lo ha extendido al caso n≥9 mediante pequeñas modificaciones.
El artículo expone en detalle la maquinaria técnica de la demostración, incluyendo las identidades de comunicación entre ceros y puntos críticos, ilustraciones con ejemplos motivadores y comparaciones con trabajos anteriores como los de Rubinstein, Brown y Xiang. Se trata de un texto técnico extenso dirigido a la comunidad matemática, centrado en la estructura lógica de la prueba más que en el anuncio del resultado.