DepescheForschung17. August 2026

Das 246-Theorem in Lean: Axiom Math legt eine maschinenprüfbare Formalisierung der schärfsten bekannten Primzahllücken-Schranke vor

Das Unternehmen Axiom Math hat eine Lean-4-Formalisierung des sogenannten 246-Theorems veröffentlicht – des Satzes, dass es unendlich viele Paare aufeinanderfolgender Primzahlen mit einem Abstand von höchstens 246 gibt. Das ist das schärfste bekannte Ergebnis auf dem Weg zur Primzahlzwillingsvermutung; es geht auf James Maynards Arbeit „Small gaps between primes“ und das Polymath8b-Projekt um Terence Tao zurück. Nach Darstellung der Projektseite hat Axioms KI-System AxiomProver die maschinenprüfbaren Lean-4-Beweise erzeugt, aufbauend auf Mathlib und der Bibliothek PrimeNumberTheoremAnd von Alex Kontorovich und Terence Tao; anschließend wurde der Code „curated and librarized“. Das Repository steht unter Apache-2.0 öffentlich und enthält neben der 246er-Schranke auch die Zwischenschranke 600 sowie Material zum Satz von Bombieri–Vinogradov. IEEE Spectrum hat den Vorgang am 17. August 2026 als Meilenstein berichtet.

Aussagen gegen die Quellen geprüft · 18. August 2026

Worum es mathematisch geht, in der Formulierung der Projektseite: „The Twin Prime Conjecture states that there are infinitely many pairs of primes that are two apart, such as (3,5), (5,7), and (11,13). This conjecture is still open, but what we currently know is that infinitely many pairs of primes are separated by no more than 246.“ Formalisiert ist die Aussage p_{n+1} − p_n ≤ 246 für unendlich viele n. Die Seite ordnet sie in die bekannte Kette ein: Yitang Zhangs erste endliche Schranke, Maynards Reduktion auf 600 und die Verfeinerung des Polymath8b-Projekts auf 246. Als Grundlagen nennt sie Mathlib und die Bibliothek PrimeNumberTheoremAnd von Alex Kontorovich und Terence Tao sowie die beiden Originalarbeiten – Maynards „Small gaps between primes“ mit den mehrdimensionalen Sieben und Polymaths „Variants of the Selberg sieve“.

Was im Repository liegt, haben wir selbst nachgesehen: `AxiomMath/PrimeGapsLib` beschreibt sich als „Public Lean library for formalizations related to prime gaps, maintained by Axiom Math“ und ist in drei Teile gegliedert – `PrimeGapsTheory` mit der Formalisierung ohne die großen numerischen Rechnungen (baut schnell), `PrimeGapsCert` mit ebendiesen Rechnungen (Bauzeit in Stunden) und `PrimeGaps` als Zusammenfassung beider. Für die Nachprüfung nennt die README zwei Wege: `lake env comparator Comparator/comparator.json` – dauert Stunden – und eine schnellere Variante mit `comparator_fast.json`, die Minuten braucht. Zusätzlich liegt in `Comparator/Challenge.lean` eine eigenständige, nur von Mathlib abhängige Fassung der ersten Aussage, deren Beweis als Platzhalter offen bleibt. Wichtig für das Verständnis: Dieses offene `sorry` ist die gestellte Aufgabe, an der sich Dritte messen können, keine Lücke in den Beweisen der Bibliothek. Die Lizenz ist Apache-2.0; ausgewiesen sind drei Hauptergebnisse rund um den Satz von Bombieri–Vinogradov und die Schranken 246 und 600.

Wie Axiom die Rolle der KI beschreibt: „AxiomProver is Axiom Math's AI system for mathematical research“, und es habe „machine-checkable Lean 4 proofs built on Mathlib“ hervorgebracht; danach sei der Code kuratiert und in Bibliotheksform gebracht worden. Eine Quantifizierung des Automatisierungsanteils steht dort nicht. IEEE Spectrum berichtet, das System habe den Beweis „for the first time“ automatisch verifiziert, und zitiert Ken Ono, Gründungsmathematiker bei Axiom Math: „This theorem currently represents the threshold of human knowledge about prime numbers“ – sowie, allgemeiner, „The world is about to run on computer code that nobody has read.“ Der zweite Zeuge des Artikels, Sidharth Hariharan, ist Doktorand an der Carnegie Mellon University und inzwischen Praktikant bei Axiom; er hält die Formalisierung für umfassender als frühere Anläufe. Als Vergleichsfall nennt der Artikel die Formalisierung von Maryna Viazovskas Beweis durch Math, Inc.

⚠️ Zur Beleglage: Projektseite und Repository sind Primärquellen des Anbieters, die einzige von uns geöffnete unabhängige Rezeption ist IEEE Spectrum – und auch dort kommt kein Fachmann zu Wort, der nicht bei Axiom Math beschäftigt oder als Praktikant angebunden wäre. Wir haben den Lean-Bau nicht selbst ausgeführt; ob die Bibliothek durchläuft und frei von offenen Beweislücken ist, können wir aus eigener Anschauung nicht bestätigen, und weder Projektseite noch README behaupten es ausdrücklich. Kennzahlen fehlen vollständig: keine Zeilenzahl, keine Rechenzeit, keine Projektdauer, keine Angabe zum Verhältnis von Maschine und Mensch. Ein Preprint gibt es nach unserer Prüfung nicht; die als PDF verlinkte Blueprint-Datei haben wir nicht geöffnet. Die Beitragendenliste der Projektseite haben wir bewusst nicht ausgezählt – zwei Abrufe unseres Werkzeugs lieferten unterschiedliche Zahlen, weshalb wir gar keine nennen; als Principal Investigators sind Letong Hong und Shubho Sengupta ausgewiesen. Die Einordnung „zum ersten Mal“ ist die Formulierung von IEEE Spectrum beziehungsweise Axiom Math, nicht unsere: Wir haben nicht geprüft, ob es frühere, unvollständige Formalisierungsanläufe zu diesem Satz gab.

// Einordnung der Redaktion

Warum das relevant ist

Hier wird eine andere Fähigkeit sichtbar als in unseren bisherigen Einträgen zu KI und Mathematik. Anthropics Zeta-Ergebnis und OpenAIs zehn Resultate waren neue Sätze mit beigelegtem Lean-Zertifikat; hier geht es umgekehrt um die Übersetzung eines bekannten, notorisch technischen Beweises in eine Form, die eine Maschine prüfen kann. Genau diese Lücke ist der eigentliche Engpass: Formalisierung galt bislang als jahrelange Handarbeit ganzer Kollektive – die Formalisierung des Vierfarbensatzes oder von Perelmans Arbeit sind Jahrzehnt-Projekte gewesen. Wenn sie sich weitgehend automatisieren lässt, verschiebt das nicht die Grenze des Wissens, sondern die Grenze des Nachprüfbaren, und das ist für eine Öffentlichkeit, die zunehmend KI-erzeugte Beweise vorgesetzt bekommt, die wichtigere Achse. Der zweite Punkt ist die Form der Veröffentlichung: Das Repository liefert nicht nur Text, sondern ein Kommando – zwei Comparator-Läufe, einer in Minuten, einer in Stunden –, mit dem sich der Bau nachvollziehen lässt. Nachprüfbarkeit als Befehl statt als Versprechen. Und drittens die Vorbehalte, die dieselbe Meldung mitliefert: Es gibt keine Kennzahlen (wie viel hat die Maschine erzeugt, wie viel haben Menschen kuratiert, wie lange dauerte es, was hat es gekostet), keine unabhängige Stimme – die beiden im IEEE-Artikel zitierten Fachleute arbeiten beide bei Axiom –, und der Artikel erinnert selbst daran, dass ein Beweisprüfer kein Freibrief ist: Eine jüngere Demonstration habe gezeigt, wie sich ein Fehler in der Methode ausnutzen lässt, damit ein falscher, KI-erzeugter Beweis akzeptiert wird.