KI beweist Sendov-Vermutung mit Lean-Verifikation

Kürzlich wurde ein Meilenstein in der theoretischen Mathematik vermeldet: Die lange offene Sendov-Vermutung sowie die Phelps-Rodriguez-Vermutung wurden abschließend bewiesen. Der Durchbruch basiert auf einer innovativen Mensch-KI-Kollaboration. Der Mathematiker Lech Mazur entwickelte initial einen computergenerierten Beweis, der in der formalen Verifikationssprache Lean validiert wurde. Anschließend erfolgte die aufwendige Sichtung, Strukturierung und Vereinfachung durch ein Forscherteam, das die Kernlogik des KI-generierten Ansatzes isolierte und in einen für die Fachwelt publizierbaren Rahmen stellte. Der neu vorgelegte Beweis zeichnet sich durch bemerkenswerte Strenge und Zugänglichkeit aus. Im Gegensatz zu früheren Ansätzen verzichtet er vollständig auf schwere analytische Methoden und stützt sich ausschließlich auf den Fundamentalsatz der Algebra sowie elementare Ungleichungen, darunter die Maclaurin-Ungleichung. Die gesamte Argumentation wurde erfolgreich in Lean formalisiert. Dabei konnte der ursprüngliche Code von rund 90.000 auf etwa 15.000 Zeilen komprimiert werden, was die Nachvollziehbarkeit und maschinelle Überprüfbarkeit signifikant erhöhte. Inhaltlich behandelt die Vermutung die geometrische Beziehung zwischen den Nullstellen und den kritischen Punkten von Polynomen, deren Nullstellen in der komplexen Einheitskreisscheibe liegen. Die Resultate bestätigen, dass zu jeder Nullstelle stets eine kritische Stelle in unmittelbarer räumlicher Nähe existiert, abgesehen von speziellen Randfällen. Der Beweis löst nicht nur die Hauptprobleme, sondern liefert zudem einen vollständig neuen, elementaren Nachweis für den bereits bekannten Satz von Rubinstein. Die Veröffentlichung unterstreicht den wachsenden Einfluss formaler Verifikation und künstlicher Intelligenz auf die moderne Wissenschaft. Während KI-Systeme zunehmend zur Generierung komplexer Beweisstränge und zur Reduktion von Formalisierungsarbeiten beitragen, bleibt die menschliche Expertise für die konzeptionelle Einordnung, die Beweissicherung und die Abgrenzung zu verwandten offenen Problemstellungen unverzichtbar. Die vorgestellte Methodik zeigt zwar klare Grenzen für weiterführende Vermutungen wie die von Borcea oder Schmeisser, etabliert aber ein skalierbares Muster für die Zusammenarbeit von Menschen und Algorithmen in der reinen Forschung. Für die wissenschaftliche Community markiert die Arbeit einen klaren Paradigmenwechsel hin zu hybrid formalen Beweisen. Die vollständige Dokumentation steht aktuell als Preprint zur Verfügung und bildet die Grundlage für künftige Analysen zu verwandten Fragestellungen in der Polynomtheorie und komplexen Analysis.