Es könnte der Beginn einer neuen Ära in der Mathematik sein – einer, die sich etliche Forscherinnen und Forscher seit Langem wünschen. Einer Zeit, in der Ergebnisse blitzschnell und stichhaltig überprüft werden können. Das würde die Arbeit vieler erleichtern: Wer publiziert, kann sicher sein, dass der Beweis korrekt ist und andere unmittelbar darauf aufbauen können. Und Gutachterinnen und Gutachter könnten sich stärker auf die Einordnung konzentrieren: Wie bedeutend ist diese Arbeit? Welchen Beitrag leistet sie zum Fach?

Zwar gibt es seit Jahrzehnten Computerprogramme, die eine mathematische Argumentationskette (also etwa einen Beweis) prüfen. Doch das eigentliche Problem liegt woanders: Es ist enorm aufwendig, die menschliche Beweissprache in die strenge Programmiersprache des Computers zu übersetzen. Diese Übersetzung, das sogenannte Formalisieren, dauert mitunter Monate oder gar Jahre – die Mühe schreckt viele Fachleute bislang ab.

Mit den ersten großen Sprachmodellen wuchs die Hoffnung. Vielleicht könnten Maschinen künftig zwischen der Sprache der Mathematiker und der formalen Sprache der Beweisprüfer übersetzen – und den Aufwand dramatisch senken. Die Umsetzung ist allerdings nicht ganz einfach. Denn anders als menschliche Sprachen wie Deutsch oder Englisch, erlaubt die formale Programmiersprache keinerlei Varianz. Jeder Begriff, jedes Symbol, jede Referenz muss exakt sitzen.

Inzwischen meldet das Start-up Math Inc. erste Erfolge: Mit seiner KI namens Gauss habe es zwei aufwendige Beweise der Mathematikerin Maryna Viazovska formalisiert, für die sie 2022 die Fields‑Medaille erhielt. Doch statt in Jubel auszubrechen, hielt sich die Begeisterung der Mathematik-Community zunächst in Grenzen. Denn das Projekt verlief nicht so, wie es sich die Fachwelt erhofft hatte.

Wie packt man Kugeln am besten zusammen?

Während seines Studiums am Imperial College in London ergriff Sidharth Hariharan im Jahr 2023 die Gelegenheit zu einem Auslandssemester an der EPFL in Lausanne. Dort hielt der Mathematiker Kevin Buzzard, ebenfalls vom Imperial College, eines Tages einen Vortrag zum Thema Lean, einer weitverbreiteten Form der Formalisierung, an der auch Hariharan arbeitete. »Es war ein bekanntes Gesicht in einem fremden Land«, erinnert sich Hariharan, »also ging ich hin«.

Anschließend machte ihn Buzzard mit Viazovska bekannt. »Ich fragte sie, warum sie an dem Vortrag teilgenommen hatte«, sagt Hariharan. Die Mathematikerin antwortete, sie sei neugierig; sie wolle verstehen, wie Formalisierung insbesondere mit Lean funktioniert. Hariharan witterte eine Chance: Er schlug vor, sie solle ihm Mathematik erklären, während er ihr Lean beibringe.

Viazovska war zu diesem Zeitpunkt eine zentrale Figur der Mathematik. Ihr war es 2016 gelungen, eine jahrzehntealte Vermutung zu lösen, nachdem viele andere aufgegeben hatten. Das Problem geht auf eine uralte Fragestellung zurück: Wie kann man Kugeln möglichst platzsparend im Raum anordnen? Die Frage klingt zwar einfach, doch um die platzsparendste Lösung zu finden, muss man erst einmal beweisen, dass alle anderen unendlich vielen Anordnungen mehr Raum erfordern. Erst 1998 gelang der Beweis, dass die pyramidenförmige Variante – wie beim Orangenstapeln auf dem Markt – im dreidimensionalen Raum tatsächlich die dichteste ist.

Doch Mathematikerinnen und Mathematiker gaben sich mit dieser Antwort nicht zufrieden. Was ist mit höheren Dimensionen? Wie sieht die dichteste Anordnung in vier, fünf oder noch mehr Dimensionen aus?

Die Antworten fallen in höherdimensionalen Räumen deutlich komplizierter aus, weil diese mehr Anordnungen und Symmetrien zulassen. Zugleich nehmen die Abstände zwischen den Kugeln in gewisser Weise zu: So ist der kleinste achtdimensionale Würfel, der eine achtdimensionale Kugel umschließt, zu 98 Prozent mit Leerraum gefüllt, während es im dreidimensionalen Raum nur 47 Prozent sind.

In den 1960er‑Jahren deutete sich an, dass für den acht‑ und den 24‑dimensionalen Raum eine besonders elegante Lösung existieren könnte. Überträgt man die platzsparendste dreidimensionale Anordnung in diese hohen Dimensionen, sind die Lücken zwischen den Kugeln exakt so groß, dass jeweils eine weitere Kugel hineinpasst. Im Acht- und 24-Dimensionalen gab es also je einen Kandidaten für die optimale Anordnung. Es fehlte nur der Beweis.

Hier kam Viazovska ins Spiel. Ein Kollege überredete sie, sich mit ihm und einem weiteren Mathematiker dem achtdimensionalen Fall zu widmen. Nach ersten, zähen Versuchen gaben die beiden Männer auf – Viazovska arbeitete weiter. Zwei Jahre lang feilte sie an der Idee, bis ihr der Durchbruch gelang: Sie hatte bewiesen, dass die achtdimensionale Anordnung tatsächlich optimal war.

Sofort machte ihre Arbeit in der Mathematik-Community die Runde. Noch am selben Abend ihrer Veröffentlichung erhielt sie die begeisterte E-Mail ihres Fachkollegen Henry Cohn, der vorschlug, gemeinsam den 24‑dimensionalen Fall anzugehen. Zwar sei sie erschöpft gewesen und wollte sich erholen, doch binnen einer Woche konnte sie mit ihren Kollegen Cohn, Abhinav Kumar, Stephen Miller und Danylo Radchenko ihren Ansatz auf 24 Dimensionen erweitern. Diese Leistungen brachten ihr schließlich die Fields‑Medaille ein.

Zwei Mathematiker, von Neugier getrieben

Genau diese Mathematik faszinierte Hariharan. Er begann, sich an der EPFL regelmäßig mit Viazovska auszutauschen. »Meine Motivation war, die Mathematik zu lernen, und ihre Motivation war es, Lean zu verstehen«, sagt er. »Wir waren einfach zwei neugierige Menschen, die etwas lernen wollten – so fing es an.« Bald entschieden sie, Viazovskas Beweis zu formalisieren.

Das Ziel war ehrgeizig. Jeder Begriff, jede Definition, jedes Theorem, auf das verwiesen wird – alles muss in Lean‑Code übersetzt werden. Zwar gibt es inzwischen eine umfangreiche Datenbank mit mathematischen Bausteinen, aber sie ist weit davon entfernt, das gesamte Wissen des Fachs abzudecken. Einige Forschende haben sich genau diesem Ausbau verschrieben.

Hariharan, heute an der Carnegie Mellon University, ließ sich von der Komplexität des Projekts nicht abschrecken. Er widmete ihm unter anderem seine Masterarbeit. Zusammen mit Viazovska und den Mathematikern Christopher Birkbeck von der University of East Anglia, Seewoo Lee von der University of California in Berkeley und Bhavik Mehta vom Imperial College London machte er im Juni 2025 das Formalisierungsprojekt öffentlich. Die Fachleute haben hierfür Viazovskas ursprüngliche Arbeit in viele kleine Teilaufgaben zerlegt, online dokumentiert und zur Mitarbeit freigegeben – die Community konnte sich Bausteine reservieren und abarbeiten. Weil das Projekt moderne und prestigeträchtige Mathematik enthielt, erregte es die Aufmerksamkeit der Lean-Community, und es gab schnell Fortschritte. Unterdessen nahmen andere Bemühungen Fahrt auf.

Eine KI erledigt die anstrengende Arbeit

»Haben Sie schon einmal Lean‑Code gesehen?«, fragte der Mathematiker und Physiker Yang Hui He einmal im Interview mit »Spektrum.de«. »Er ist nicht für Menschen gemacht.«

Das sah der Mathematiker Auguste Poiroux von der EPFL ähnlich. Er ist Mitglied erster Stunde des im August 2025 gegründeten Start-ups Math Inc. Das Ziel: Autoformalisierung. »Wir wollen es ermöglichen, die Inhalte eines Papers oder eines Buchs automatisch in Lean‑Code zu übertragen und sofort prüfen zu können«, erklärt Poiroux.

Die mühselige Übersetzung soll durch Maschinen unterstützt werden, damit sich Fachleute wieder mehr auf Inhalte konzentrieren können. Die technische Lösung hatten die Gründer schon im Gepäck: »Gauss«, ein agentenbasiertes Sprachmodell. »Als wir im Sommer 2025 an die Öffentlichkeit gingen, bekamen wir viel Aufmerksamkeit«, erinnert sich Poiroux. Als Test ließ das Team einen klassischen Beweis – den Primzahlsatz – formalisieren. »Das funktionierte, aber nur mit menschlicher Unterstützung«, sagt er. »An einigen Stellen mussten wir die KI anleiten und mehr Details nachliefern.«

»Plötzlich gab das System den gesamten formalisierten Beweis aus. Das hat uns total überrascht!«Auguste Poiroux, Mathematiker

Math Inc. wurde auf das Projekt von Hariharan und seinen Kolleginnen und Kollegen aufmerksam und nahm Kontakt auf. »Im Herbst 2025 sagten uns die Leute von Math Inc., dass sie kleinere Teile unseres Projekts formalisieren konnten, und teilten einige ihrer Ergebnisse mit uns«, erinnert sich Hariharan. »Dann verstummte der Austausch. Wir wussten nicht, wie weit sie waren – oder ob sie überhaupt noch daran arbeiteten.«

»Wir waren ein sehr kleines Team«, sagt Poiroux. »Wir merkten, dass wir nicht zugleich unser System verbessern und am Projekt von Hariharan arbeiten konnten. Also konzentrierten wir uns auf die KI.« In den folgenden Wochen entwickelten sie Gauss weiter. Schließlich schien die Software in der Lage, eine mathematische Arbeit ohne menschliche Hilfe in Lean‑Code zu übertragen und automatisch zu prüfen. »Wir nahmen Viazovskas achtdimensionalen Beweis als Test«, sagt Poiroux. »Und plötzlich gab das System den gesamten formalisierten Beweis aus. Das hat uns total überrascht!«

Ein Vorstoß, der aneckt

Poiroux und seine Kollegen waren begeistert. Das waren nicht alle. Als er Viazovska von dem Ergebnis erzählte, hielt sich ihre Freude in Grenzen. »Wir waren, gelinde gesagt, sehr überrascht. Wir haben das nicht kommen sehen«, sagt Hariharan. »Es war unser Projekt, wir haben zwei Jahre lang viel Arbeit hineingesteckt – und dann löst es Math Inc.«

Besonders ärgerlich sei hierbei gewesen, dass ein Teil der Formalisierung eigentlich als Bachelorarbeit für einen italienischen Studenten geplant war. »Er muss sich jetzt ein neues Thema suchen.«. Hätte Hariharan von den Plänen des Start-ups gewusst, hätte er Poiroux und seine Kollegen wenigstens darüber informieren können und sie darum bitten, diesen Baustein für den Studenten offen zu lassen. »Aber so ist das wohl, KI ist disruptiv.«

»In der Aufregung haben wir die Konsequenzen nicht vollständig durchdacht«, sagt Poiroux. »Das war so nicht geplant. Wir haben sogleich unsere Ergebnisse mit dem Team geteilt. Ich verstehe, dass es von außen so ausgesehen haben könnte, als hätten wir unseren Fortschritt absichtlich geheim gehalten. Wir werden in Zukunft auf jeden Fall vorsichtiger sein.«

Kurz nach dem ersten Erfolg nahm sich Math Inc. den zweiten Viazovska‑Beweis vor – den zur optimalen Kugelpackung in 24 Dimensionen. »In diesem Fall gaben wir Gauss nur das Paper, sonst nichts«, sagt Poiroux. Anders als im achtdimensionalen Fall habe es dazu keine menschliche Vorarbeit gegeben. »Und das System verwandelte es in rund 120 000 Zeilen Lean‑Code.« Der Code wurde inzwischen geprüft – er ist korrekt.

Damit sind nun beide Ergebnisse von Viazovska formalisiert und verifiziert. Ein gewaltiger Fortschritt für die Lean-Community.

Die Zukunft der Mathematik

Inzwischen arbeitet Math Inc. mit Hariharan und weiteren Fachleuten zusammen, um die Autoformalisierung weiter voranzubringen und Werkzeuge wie Gauss nutzerfreundlicher zu gestalten. Forschende sollen etwa besser mit dem System interagieren können. Zudem soll der von der KI erzeugte Lean‑Code verbessert werden. »Auch wenn der Code fehlerfrei ist, enthält er Redundanzen und lässt sich teilweise drastisch vereinfachen«, sagt Hariharan. »So, wie er jetzt ist, würde ihn die Lean‑Community nicht ohne Weiteres in ihre Datenbank aufnehmen.«

»Da Gauss nun in der Lage ist, Mathematik auf Spitzenniveau autonom zu formalisieren, konzentrieren wir uns nun auf größere Teile der Mathematik«, bekräftigt Poiroux. Paper, Beweise, Definitionen: Immer mehr soll in Lean übersetzt werden. Denn erst dann lassen sich neue Arbeiten problemlos durch Programme wie Gauss prüfen. »Für viele Gebiete fehlen die Bausteine in Lean noch – solche Beweise könnten wir derzeit gar nicht formalisieren«, sagt er.

»Wenn unsere Modelle die Mathematik in der Breite kennen, können sie ganz anders darüber nachdenken – und womöglich völlig neue Resultate liefern«Auguste Poiroux, Mathematiker

Wenn aber große Teile der Mathematik formalisiert sind, eröffnen sich neue Möglichkeiten. Denn die Systeme von Math Inc. sind mehr als bloße Übersetzungsmaschinen: Sie können kleinere Fehler in Arbeiten erkennen und beheben. »Autoformalisierung ist nicht einfach nur Übersetzung. Oftmals müssen dabei erhebliche Beweislücken geschlossen werden, was Fähigkeiten zum Beweisen von Theoremen erfordert, die weit über das Lösen von Aufgaben der Mathematikolympiade hinausgehen«, stellt Poiroux fest. »Wenn unsere Modelle die Mathematik in der Breite kennen, können sie ganz anders darüber nachdenken – und womöglich völlig neue Resultate liefern.«

Vorerst gelten Systeme wie Gauss als reine Hilfsmittel: Sie befreien Fachleute vom Prüfen und schaffen Raum für Ideen. Zugleich weisen sie auf eine Zukunft hin, in der eine überlegene KI die gesamte Mathematik überblickt – und Menschen bei der Forschung eventuell den Rang abläuft.