Dimensionsreduktionsschlag, ein Mathematikdoktor mit glühendem Kopf vor Anstrengung, ein KI-Mathematiker: morgens Aufgaben stellen, um 16 Uhr den Beweis abgeben
Seit Februar dieses Jahres hat AxiomProver 8 AI-Papiere in den härtesten Bereichen auf arXiv erscheinen lassen, und 6 weitere sind in Vorbereitung. Dieser Rhythmus, in dem man am Vormittag die Aufgabe stellt und am Nachmittag die Lösung abgibt, lässt die Zeiten, in denen Doktoranden vor Kopfschmerzen bange waren und Professoren um die Beförderung ringen mussten, für immer hinter sich. Was kann nun die KI noch leisten?
Die Mathematiker können nicht schlafen!
Stellen Sie sich vor, Sie sind ein Gutachter.
Eines Tages liegt ein Papier in Ihren Händen. Es behauptet, ein Problem zu lösen, das die Kollegen seit Jahrzehnten plagt.
Sie holen tief Luft, machen sich einen Kaffee und beginnen Zeile für Zeile zu prüfen – das kann Monate oder sogar Jahre dauern.
Das ist keine Übertreibung.
In der Mathematik ist es gang und gäbe, dass es zwei bis drei Jahre dauert, bis ein anspruchsvolles Papier von der Einreichung bis zur Veröffentlichung geht.
Die gesamte moderne Mathematik basiert auf einem äußerst teuren, äußerst langsamen und manchmal fehlerhaften "menschlichen Vertrauenssystem".
Hinter jedem "richtigen" Ergebnis steht ein müder und übermüder menschlicher Experte, der es bescheinigt.
Jetzt sagt der Mathematiker Ken Ono: Dieses System muss aufgerüstet werden.
Ken Onos Worte haben viel Wert. Der ehemalige Präsident der amerikanischen Mathematischen Gesellschaft, Ken Ribet, hat ihn als "Legende der Mathematik" bezeichnet.
Ken Ono ist bekannt für seine eingehende Untersuchung der Theorien des indischen Mathematikgenies Srinivasa Ramanujan. Er hat auch ein erstklassiges amerikanisches Bachelor-Forschungsprogramm geleitet und 10 Gewinner des Morgan-Preises ausgebildet. Hong Letong, ein 00er aus Guangzhou und Gründer von Axiom, ist einer von ihnen.
Eine KI, die ein Problem in einem Vormittag lösen kann
Dieses KI-Tool heißt AxiomProver.
Wie stark ist es?
Berichten zufolge sind seit Februar dieses Jahres 8 Papiere still und leise auf arXiv (dem Ort, an dem Mathematiker weltweit ihre Preprints veröffentlichen) erschienen, die die Bereiche algebraische Geometrie, Darstellungstheorie, Zahlentheorie und Kombinatorik abdecken, die härtesten Gebiete der Mathematik.
5 von ihnen wurden von renommierten mathematischen Zeitschriften angenommen, mehrere weitere befinden sich in der Prüfung, und 6 sind in Vorbereitung.
Nach ihrem Wissen ist es das erste Mal in der Geschichte, dass "Papier + formales Beweiszeugnis" auf diese Weise in die Zeitschriftenliteratur eingeführt wird.
Was aber wirklich die Haare zu Berge stehen lässt, ist die Geschwindigkeit.
Manchmal gibt ein Mathematiker dem System um 10 Uhr morgens ein noch ungelöstes offenes Forschungsproblem. Um 16 Uhr am selben Tag kann die KI eine vollständige, maschinell verifizierte Lösung liefern.
Am Vormittag die Aufgabe stellen, am Nachmittag die Lösung abgeben. Dazwischen ist nur ein Mittagessen.
Früher wäre das ein Ergebnis gewesen, das Doktoranden vor Kopfschmerzen gebracht und Professoren zur Beförderung geführt hätte.
Warum kann es "nicht falsch rechnen"?
Hierbei könnten Sie möglicherweise die Stirn runzeln: Rechnet die KI nicht oft anmaßend Unsinn? Warum sollte man ihr vertrauen?
Eine gute Frage. Dies ist genau der entscheidende Punkt.
Ein normales Large Language Model (also die Art von Chat-KI, die Sie täglich verwenden) "errät" im Wesentlichen das nächstwahrscheinlichste Wort.
Je öfter man rät, desto wahrscheinlicher macht man Fehler – als sie auf den Markt kamen, konnten sie nicht einmal einfache Schulrechnungen richtig machen und wurden lange Zeit ausgelacht.
Aber AxiomProver geht einen anderen Weg. Alle von ihm generierten Beweise sind in einer formellen Sprache namens Lean geschrieben.
Was ist Lean?
Sie können es sich als einen unerbittlichen und gefühlslosen Maschinenrichter vorstellen.
Ihm ist es egal, wie elegant Ihr Beweis liest oder wie klug Ihre Idee ist. Er akzeptiert nur eines: Ist jeder Schritt der Argumentation logisch lückenlos? Fehlt ein Zeichen, tut es leid, nicht bestanden.
Deshalb hängt die "Richtigkeit" der Beweise von AxiomProver nicht mehr von einem menschlichen Experten ab, der nachts wach bleibt, um sie zu prüfen, sondern wird direkt von der Maschine bescheinigt.
Es kann nicht herumkommen, denn sobald es einen Fehler macht, weiß die Maschine es sofort.
Menschliche Gutachter können müde, schläfrig und unaufmerksam werden. Der Maschinenrichter nicht.
Die "Vertrauenskrise" und die "Geschwindigkeitsengstelle" der Mathematik brechen zusammen
Jetzt können wir die wirkliche Bedeutung dieses Vorgangs aufdecken.
Die wissenschaftliche Entdeckung ist seit langem an zwei hartnäckigen Problemen hängen geblieben.
Das erste ist die Vertrauenskrise.
Ob ein mathematischer Beweis richtig ist, muss letztendlich von Menschen entschieden werden. Aber Menschen können Fehler machen, haben Interessen und begrenztes Energiebudget. Dieses "menschliche Vertrauenssystem" ist im Wesentlichen fragil.
Das zweite ist die Geschwindigkeitsengstelle.
Das Gutachten kann Jahre dauern, nicht weil die Gutachter faul sind, sondern weil das menschliche Gehirn einfach so langsam rechnet. Selbst das klügste Gehirn hat nur 24 Stunden am Tag.
Die Vorgehensweise von AxiomProver ist wie ein Schuss auf diese beiden Probleme.
Das Vertrauensproblem wird an die Maschine übergeben: Das Siegel des Lean-Checkers ist zuverlässiger als das eines menschlichen Experten.
Das ist der Grund, warum das Gutachten in den Zeitschriften so unglaublich schnell gehen kann – die Gutachter müssen nicht mehr von Grund auf prüfen, sondern müssen nur entscheiden, ob das Ergebnis wichtig und gut geschrieben ist.
Das Geschwindigkeitsproblem wird an die Rechenleistung übergeben: Die Möglichkeit, am Vormittag die Aufgabe zu stellen und am Nachmittag die Lösung abzugeben, war in der menschlichen Ära undenkbar.
Die KI hat diesmal in der Mathematikwelt ein Erdbeben ausgelöst.
Im Oktober letzten Jahres behauptete OpenAI, dass GPT-5 10 Erdős-Probleme "gelöst" habe.
Die Mathematikwelt rief Betrug. Demis Hassabis nannte es "peinlich".
Sieben Monate später veröffentlichten OpenAI und DeepMind in derselben Woche beide verifizierte mathematische Durchbrüche.
Was Axiom erreichen will, ist es, die Mathematik aus der "Handwerks"-Ära in die industrielle Ära der "sofortigen Verifikation und maschinellen Bescheinigung" zu bringen.
Was kann die KI noch leisten?
Quellen:
https://x.com/axiommathai/status/2059640252546126087?s=20https://www.axios.com/2026/05/26/axiom-ai-math-journalhttps://axiommath.ai/papers
Dieser Artikel stammt aus dem WeChat-Account "Xinzhiyuan", geschrieben von ASI Revelation, redigiert von David, und wurde von 36Kr mit Genehmigung veröffentlicht.