Die KI von Axiom Math verifiziert den 246‑Primzahllücken‑Satz in Lean

Axiom Math sagt, dass sein AxiomProver‑System einen maschinell geprüften Lean‑4‑Beweis des bislang stärksten bekannten Ergebnisses zu Lücken zwischen Primzahlen erzeugt hat: den Satz, dass unendlich viele Primzahlpaare sich um höchstens 246 unterscheiden. Das Unternehmen veröffentlichte das Ergebnis am 17. August 2026 als interaktive Formalisierungs‑Blueprint, die 41 namentlich genannte mathematische, ingenieurwissenschaftliche und leitende Forschende ausweist, wobei IEEE Spectrum zuerst darüber berichtete.

Die Schranke von 246 stellt derzeit die Grenze des menschlichen Wissens im langjährigen Angriff auf die Zwillingsprimzahl‑Vermutung dar, die im 19. Jahrhundert formulierte Hypothese, dass Primzahlen, die sich genau um zwei unterscheiden, unendlich oft vorkommen. Die Projektseite von Axiom Math beschreibt die Arbeit als eine einheitliche Formalisierung von James Maynards 2013‑Papier „Small gaps between primes“ zusammen mit dem Teil der Folgestudie der Polymath8b‑Kollaboration, der Maynards Schranke von 600 auf 246 verschärfte. Die maschinell geprüften Beweise sind in einer öffentlichen Lean‑Bibliothek, PrimeGapsLib, organisiert, wobei der 246‑Satz ihr Flaggschiff‑Ergebnis ist.

„Dieser Satz stellt derzeit die Grenze des menschlichen Wissens über Primzahlen dar“, sagte Ken Ono, der Gründungs­mathematiker von Axiom Math.

Formale Verifikation bedeutet, einen Beweis in eine Sprache zu übersetzen, die ein kleines, vertrauenswürdiges Programm – ein Kernel – Zeile für Zeile prüfen kann. Das Ergebnis ist keine absolute Garantie – die Aussage selbst muss korrekt übersetzt werden, und der Prüfer muss zuverlässig sein – aber es eliminiert die Fehlbarkeit des menschlichen Schiedsrichters aus der Kette. Bisher wurden KI‑Systeme, die bei mathematischen Benchmarks konkurrieren, meist anhand von Wettbewerbsaufgaben mit kurzen, eigenständigen Beweisen gemessen; die Lücke zwischen diesen Ergebnissen und der Formalisierung auf Forschungsniveau war groß, ein Muster, das in früheren Systemen, die in der Olympiade‑Geometrie herausragten sichtbar ist, während die Forschungsmathematik weitgehend unberührt blieb.

Von 70 Millionen zu 246

Die Vermutung selbst, exakt formuliert von Alphonse de Polignac im 19. Jahrhundert, bleibt unbewiesen. Die erste endliche Schranke jeglicher Art erschien 2013, als Yitang Zhang bewies, dass unendlich viele Primzahlpaare sich innerhalb von 70 Millionen voneinander befinden. Monate später stellte Maynard eine verfeinerte Siebmethode vor und senkte die Schranke auf 600 – eine Arbeit, die zu seiner Fields‑Medaille 2022 beitrug – und die Polymath8b‑Kollaboration, zu der Maynard und Terence Tao gehörten, drückte sie auf 246. Der Blueprint von Axiom Math stellt diesen Fortschritt als das Projekt dar, das es zu formalisieren beabsichtigte.

Die Formalisierung folgt einer Pipeline, die das Unternehmen in drei Phasen beschreibt. Die Forschenden verfassten zunächst den Beweis als Blueprint – jede Definition, jedes Lemma und jeder Satz erhielt ein Label, eine präzise Formulierung und eine Liste der abhängigen Ergebnisse – und erzeugten damit einen Abhängigkeitsgraphen, der die Arbeit ordnete. AxiomProver, das Multi‑Agent‑System des Unternehmens für mathematische Forschung mittels formaler Beweise, erzeugte anschließend maschinenprüfbare Lean‑4‑Beweise, die auf Mathlib, der Community‑Mathematik‑Bibliothek, und auf PrimeNumberTheoremAnd, dem bestehenden Formalisierungs‑Projekt unter Leitung von Alex Kontorovich und Tao, aufbauen. Das Axiom‑Team prüfte dann den generierten Code und organisierte ihn in PrimeGapsLib.

Die in der Bibliothek angegebenen Hauptresultate gehen leicht über den Titel‑Satz hinaus. Neben der Schranke von 246 formalisiert sie Maynards Schranke von 600 und enthält eine eigenständige Verifikations‑Challenge – ausschließlich auf Mathlib aufgebaut, wobei der Beweis‑Slot leer bleibt – die jedem mit dem Lean‑Comparator‑Tool ermöglicht, unabhängig zu bestätigen, dass die Bibliotheks‑Beweise den angegebenen Sätzen entsprechen. Das Unternehmen warnt, dass die vollständige Prüfung Stunden dauern kann; eine reduzierte Version, die die beiden anderen Resultate abdeckt, läuft in Minuten.

Wo das im Kontext von KI‑Formaliserungs‑Behauptungen steht

Das Ergebnis erscheint in einem Jahr zunehmender Behauptungen, dass KI‑Systeme Mathematik auf Forschungsniveau betreiben, wobei die meisten an Wettbewerbs‑Scores oder kurzen Beweisen ausgerichtet sind. Axiom Math ist einer der aggressiveren Behauptenden: AxiomProver wird zugeschrieben, zuvor offene Probleme gelöst zu haben, einschließlich Arbeiten, die das Unternehmen in peer‑reviewten Zeitschriften veröffentlicht hat, und KI‑Systeme haben nun mehrere langjährige Erdős‑Probleme gelöst. Die Formalisierung von 246 ist eine andere Art von Ergebnis – kein neuer Satz, sondern eine maschinell geprüfte Rekonstruktion eines der technisch anspruchsvollsten Beweise der modernen Zahlentheorie.

Der engste Vergleich liegt Anfang dieses Jahres, als Math, Inc. seinen Gauss‑Agenten einsetzte, um den formalen Beweis von Maryna Viazovskas mit dem Fields‑Medaille‑gekrönten Kugelpackungs‑Ergebnis in den Dimensionen 8 und 24 abzuschließen. Sidharth Hariharan, der Ph‑D‑Student der Carnegie Mellon University, der die menschliche Blueprint‑Arbeit an dieser Formalisierung leitete und jetzt Praktikant bei Axiom Math sowie benannter mathematischer Mitwirkender am 246‑Projekt ist, argumentiert, dass das neue Ergebnis die umfassendere Errungenschaft sei. Seine Begründung, wie er sie beschrieb, lautet, dass Axiom für Wiederverwendung gebaut hat: statt einer einmaligen Formalisierung eines einzelnen Beweises ist PrimeGapsLib eine gepflegte Bibliothek von Primzahllücken‑Ergebnissen, die zukünftige Formalisierungs‑Arbeiten und Forschung unterstützen soll.

Diese Unterscheidung ist wichtig für die Interpretation des Ergebnisses. Eine einmalige Verifikation zeigt, dass ein System mit einem harten Beweis umgehen kann. Eine Bibliothek demonstriert etwas, das eher einer Infrastruktur entspricht – wiederverwendbare formale Werkzeuge, auf denen andere Ergebnisse aufbauen können – was die Richtung ist, in die formale Beweissysteme sich bewegen, während sie vom Lösen von Übungsaufgaben zum Prüfen echter Mathematik übergehen. Der Fähigkeitsanspruch beruht hier auf Artefakten, die öffentlich und wieder ausführbar sind, nicht auf einem Benchmark‑Score: der Blueprint, der Lean‑Code und eine Comparator‑Challenge, die so konzipiert ist, dass externe Forschende die Beweise selbst verifizieren können.

Ono stellt die Mathematik als Testumgebung für ein größeres Ziel dar. Wenn Eigenschaften von Software – ob ein Programm terminiert, ob seine Ausgabe für jede Eingabe korrekt ist – als präzise mathematische Aussagen formuliert werden können, dann könnten, so argumentiert er, aus AxiomProver abgeleitete Systeme diese formal beweisen, was auf die Verifikation von KI‑generiertem Code hinweist, der in Infrastruktur‑, Finanz‑ und Sicherheitssystemen eingesetzt wird.

„Die Welt wird bald auf Computercode laufen, den niemand gelesen hat“, sagte Ono. „KI ist da und wir können nicht länger wegschauen – die Formalisierung von Beweisen ist ein Testfeld für die Lösung dessen, was ich für die wichtigste Herausforderung halte, der wir von KI gegenüberstehen werden.“

Für den Moment ist das Ergebnis enger gefasst und prüfbar: ein Blueprint von 41 Autor*innen, eine öffentliche Lean‑Bibliothek und ein maschinell verifizierter Beweis, dass Primzahlen, die höchstens 246 voneinander entfernt sind, niemals erschöpft sind – der am nächsten verifizierte Nachbar der Zwillingsprimzahl‑Vermutung und das tiefste Stück Forschungs­mathematik, das ein KI‑System bislang von Anfang bis Ende geprüft hat.