IA et Lean valident la résolution de la conjecture de Sendov

Une avancée majeure en mathématiques computationnelles a été annoncée avec la résolution complète des conjectures de Sendov et de Phelps-Rodriguez, des problèmes de plus de cinq décennies portant sur la répartition des zéros et des points critiques des polynômes. La preuve, initialement générée récemment par un outil d'intelligence artificielle développé par le mathématicien Lech Mazur, a été validée avec succès dans le système de vérification formelle Lean. Pour rendre cette démonstration accessible et rigoureuse, une équipe de chercheurs a consacré plusieurs jours à une étape critique de digestion et de simplification assistée par IA. Ce travail a permis de structurer les idées centrales, d'éliminer les redondances et de placer le résultat dans son contexte mathématique historique, aboutissant à une version prête pour publication. Le résultat surprend par son élégance et sa simplicité conceptuelle. Loin des analyses complexes habituellement requises pour ce type de problème, la preuve finale repose principalement sur l'algèbre élémentaire, le théorème fondamental de l'algèbre et des transformations de Möbius de base. L'inégalité la plus avancée mobilisée, l'inégalité de Maclaurin, peut d'ailleurs être dérivée de moyens élémentaires. Grâce à une automatisation intelligente, l'intégralité du raisonnement a été formalisée dans Lean en environ 15 000 lignes de code, soit six fois moins que la version initiale de près de 90 000 lignes. Cette optimisation confirme la capacité des assistants numériques à transformer des preuves brutes générées par IA en architectures mathématiques solides et vérifiables. La résolution de ces conjectures clôt définitivement un débat qui opposait la communauté mathématique depuis les années 1960. Elle démontre que les zéros d'un polynôme dont toutes les racines se trouvent dans le disque unité garantissent nécessairement l'existence de points critiques à une distance précise, sous réserve de quelques cas limites exclus. Cette percée ouvre également la voie à une réévaluation des outils numériques dans la recherche théorique. Si l'IA a brillamment réussi ici en produisant un squelette de preuve et en accélérant la vérification formelle, les mêmes techniques n'ont pas encore trouvé de prise sur les conjectures apparentes de Borcea, Schmeisser ou Smale, qui restent ouvertes. Les chercheurs soulignent que ces extensions nécessiteront des approches complémentaires, car les identités et inégalités qui ont suffi ici ne s'appliquent plus directement dans leurs cadres plus généraux. Cette réussite marque un tournant dans la collaboration homme-machine. En combinant la puissance de génération algorithmique avec l'expertise humaine de validation et de simplification, les mathématiciens prouvent que l'IA n'est pas un substitut, mais un multiplicateur de précision. À mesure que les systèmes de vérification formelle comme Lean gagnent en maturité, la frontière entre découverte assistée et preuve rigoureuse s'efface, promettant d'accélérer considérablement la résolution de problèmes longtemps considérés comme hors de portée.