Wann kann man sagen, dass eine KI einsatzbereit ist? Ein Team mit einem Schätzwert von 300 Millionen hat zwei Wörter als Antwort gegeben: "Abnahme".
Das Startup Axiom Math wurde von der 24-jährigen Carina Hong gegründet und widmet sich der Entwicklung eines "Künstlichen Intelligenz - Mathematikers", der die logische Richtigkeit autonom überprüfen kann. Das Unternehmen erhielt 2025 eine Finanzierung in Höhe von 64 Millionen US - Dollar. Das Kernteam vereint Spitzenkünstler aus Meta und Google sowie bekannte Mathematiker. Im Gegensatz zu den gängigen großen Modellen gewährleistet sein System durch die Programmiersprache Lean, dass jeder Schritt des Schlussfolgungsprozesses nachvollziehbar und überprüfbar ist, wodurch das Vertrauensproblem gelöst wird, dass die Ergebnisse der KI schwer zu überprüfen sind. Durch seine hervorragende Leistung beim Putnam - Mathematikwettbewerb hat Axiom bewiesen, dass die KI von der einfachen Antwortgenerierung zu strengen formalen Beweisen übergehen kann. Dieser Streben nach Vertrauenswürdigkeit zielt darauf ab, die KI von einem instabilen Hilfsmittel zu einem zuverlässigen Partner zu machen, der in der Forschung und in der Industrie tatsächlich eingesetzt und überprüft werden kann.
Im Jahr 2025 wurde in fast jeder KI - Präsentation gesagt: "Was können wir tun?"
Das eigentliche Problem, vor dem Unternehmen stehen, ist jedoch eine andere Frage: Wie kann man beweisen, dass die Ergebnisse der KI richtig sind?
Viele KI - Produkte werden vor dem Start gut in der Demo gezeigt, aber sobald sie in Betrieb genommen werden, treten Probleme auf:
Fehler können nicht lokalisiert werden,
Verantwortlichkeiten können nicht geklärt werden,
Ergebnisse können nicht reproduziert werden.
Am Ende kann nur gesagt werden: Die Überprüfung ist nicht möglich.
Axiom Math, ein KI - Startup mit Sitz in San Francisco, hat einen anderen Ansatz: Statt darauf abzuzielen, was die KI können kann, wird bewiesen, was sie richtig gemacht hat.
Dieses Unternehmen, das erst im Oktober 2025 die Seed - Runde der Finanzierung abgeschlossen hat (64 Millionen US - Dollar, Schätzungswert von 300 Millionen US - Dollar, angeführt von B Capital), entwickelt einen Künstlichen Intelligenz - Mathematiker, der unabhängig Antworten geben und auch die Richtigkeit selbst überprüfen kann.
Deshalb hat dieses Team eine Gruppe von Menschen mit einem sehr tiefen technischen Hintergrund angelockt: ehemalige Kernforscher von Meta FAIR und Google Brain sowie der bekannte Mathematiker Ken Ono, der Lehrer von Carina Hong an der MIT war.
Carina Hong, 24 Jahre alt.
Am 21. Dezember 2025 wurde sie von einer Medienredaktion gefragt, wie sie Mitarbeiter rekrutiere. Ihre Antwort war einfach:
Wenn das Problem schwierig genug ist, werden die Menschen von selbst zusammenkommen.
Dies ist keine leere Rede. Ihre Methode besteht darin, ein schwieriges Problem zu finden, das zehn Jahre lang gelöst werden kann, und dann auf die echten Experten zu warten, die sich von selbst melden.
24 Jahre alt, 64 Millionen US - Dollar, Schätzungswert von 300 Millionen US - Dollar.
Sie setzt nicht auf ein Produkt, sondern auf die nächste Mindestanforderung für die KI.
Abschnitt 1 | 24 Jahre alt, 300 Millionen US - Dollar Schätzungswert, sie will die KI dazu bringen, sich selbst zu beweisen
Ihr Name ist Carina Hong, und sie wurde in Guangzhou geboren.
Als Kind, als sie Mathematikolympiadeaufgaben löste, wusste sie nicht, dass sie in Zukunft in Silicon Valley über KI sprechen würde. Aber sie erinnert sich, dass es ihr jedes Mal, wenn sie eine Aufgabe gelöst hat, so gefühlt war, als würde ein Kind ein Computerspiel leveln, und sie konnte nicht aufhören.
Sie hat es von Guangzhou bis zur MIT geschafft, dann den Rhodes - Preis erhalten und in Oxford Neurowissenschaften studiert. Schließlich ist sie an die Stanford University gegangen, um ein kombiniertes Programm für einen Doktortitel in Mathematik und Rechtswissenschaft zu absolvieren.
An der MIT hat sie 20 Graduiertenkurse in Mathematik belegte, 9 Artikel veröffentlicht und auch untersucht, wie neuronale Netze Funktionen verstehen. In Oxford war sie am UCL Gatsby Institute (der Geburtsort von DeepMind) und sah erstmals aus nächster Nähe, wie die KI reale Probleme löst: Bilder, Sequenzen, Steuerungsmodelle.
Da fing sie an sich zu fragen: Wenn die KI Spiele spielen und Code schreiben kann, warum kann sie dann nicht Mathematik machen?
Der echte Wendepunkt ereignete sich in Silicon Valley.
Während ihres Promotionsstudiums an der Stanford University ging sie oft in ein Café, um Artikel zu schreiben. Bei einer zufälligen Gelegenheit lernte sie den KI - Wissenschaftler Shubho Sengupta aus dem Meta FAIR - Team kennen.
Eine war eine Mathematikerin, die wollte, dass die KI Mathematik versteht.
Der andere war ein Ingenieur, der ein Problem finden wollte, das die KI wirklich lösen sollte.
Sie haben zwei Stunden lang gesprochen, keine Projekte besprochen und auch keine Finanzierungen erwähnt. Sie haben sich nur um eine Hypothese herumgesprochen: Könnte man einen Künstlichen Intelligenz - Mathematiker bauen?
Nach diesem Gespräch fing sie an, sich ernsthaft über das zu Gedanken zu machen. Kurz darauf hat sie ihren Studienabbruch beantragt.
Sie sagte: Einige Probleme werden an der Universität zu langsam gelöst.
Was sie tun will, ist kein Chatbot und auch kein Code - Assistent, sondern ein KI - System, das Theoreme überprüfen und sogar neue Vermutungen aufstellen kann.
Dieses System heißt Axiom, was "Axiom" oder "Grundsatz" bedeutet, also der grundlegendste Ausgangspunkt der mathematischen Theorie.
Von diesem Ausgangspunkt aus wird ein ganzes System entwickelt, damit die KI auch die Grenzen der Mathematik erkunden kann.
Abschnitt 2 | 9 von 12 Aufgaben beim Putnam - Test, aber das Wichtigste ist nicht die Punktzahl
Wenn die meisten Menschen an die Möglichkeit denken, dass die KI Mathematik lernt, denken sie vielleicht an Tests und die Abgabe von Antworten.
Aber Carina sagt, das ist nur der erste Schritt. Das Wichtigste ist, ob sie weiß, ob ihre Antwort richtig ist.
Dies ist nicht nur ein mathematisches Problem, sondern auch ein engineeringmäßiges Problem. Wenn die Antworten der KI nicht überprüft werden können, können sie nicht in kritischen Szenarien eingesetzt werden.
Wenn Menschen Mathematikaufgaben lösen, haben sie einen natürlichen Vorteil: Wir können zurückschauen und überprüfen, ob es logische Lücken gibt, ob es Sprünge in der Schlussfolgerung gibt und ob die Details übereinstimmen.
Carina nennt diesen Überprüfungsprozess "Überprüfung".
Aber die großen Modelle können das nicht.
Sie generieren viel Inhalt, aber es ist schwer, dass sie selbst feststellen können, ob dieser Inhalt richtig ist. Insbesondere in der Mathematik, wenn nur ein Buchstabe falsch ist, stimmt die gesamte Schlussfolgerung nicht mehr.
Um dieses Problem zu lösen, muss man sich auf formale Sprachen verlassen.
Carinas Team nutzt eine mathematische Programmiersprache namens Lean. Alle Formeln, Schritte und Beweise müssen genauso wie in einem Programm geschrieben werden und von der Maschine überprüft werden können.
Dies bedeutet, dass es nicht darauf ankommt, was die KI sagt, sondern dass jeder Schritt nachvollziehbar sein muss und am Ende wie bei einer Software - Überprüfung validiert werden muss.
Um zu beweisen, dass diese Methode funktioniert, haben sie einen Test durchgeführt.
Im Dezember 2025 war der amerikanische Putnam - Mathematikwettbewerb gerade vorbei. Dies ist der schwierigste Mathematikwettbewerb für Studenten in den USA, an dem etwa 4.000 Teilnehmer teilnehmen. Carinas Team hat die Ergebnisse auf X veröffentlicht: AxiomProver hat 9 der Aufgaben autonom gelöst, formale Beweise in der Lean - Sprache gegeben und alle wurden erfolgreich überprüft.
Dies ist nicht nur das richtige Lösen von 9 Aufgaben, sondern dass die KI selbst die Aufgaben löst, selbst überprüft und selbst bestätigt, dass sie richtig sind.
Carina sagt:
"Wir streben nicht danach, eine KI zu entwickeln, die Antworten abschreiben kann, sondern einen Partner, der alle mathematischen Details ausarbeiten kann."
Was ist die eigentliche Bedeutung der Überprüfung?
Es bedeutet, dass die KI nicht nur eine Antwort geben muss, sondern auch beweisen muss, dass die Antwort richtig ist.
In Szenarien wie der Chip - Entwicklung, der wissenschaftlichen Forschung und dem Finanzsystem, wo die Fehlerquote sehr niedrig sein muss, haben ungenaue Antworten keinen Wert. Die KI muss in der Lage sein, den Lösungsweg zu geben, die Denkweise zu erklären und der Überprüfung zu unterziehen.
Nur wenn die KI überprüft werden kann, kann man ihr vertrauen.
Abschnitt 3 | Warum verlassen sich Leute von Meta und Google ihren Job und kommen hierher?
Welches Team braucht man, um dies zu erreichen?
Dieses Team ist nicht groß, es gibt derzeit nur 17 Mitglieder, aber jeder, der beigetreten ist, ist ein Spitzenforscher in seinem Bereich.
Der CTO Shubho Sengupta wurde von Carina in einem Café in der Nähe der Stanford University zufällig getroffen. Er war ursprünglich bei Meta FAIR, hat das Team geleitet, das OpenGo und CrypTen entwickelt hat, und hat auch an der frühen CUDA - GPU - Architektur beteiligt. Er kennt die Probleme der großen Modelle und auch, warum der mathematische Bereich schwierig ist.
Aber in großen Unternehmen sind die Ziele zu verteilt. Er wollte einen Ort finden, an dem er sich auf ein extrem schwieriges Problem konzentrieren kann.
Ein anderer Kernmitglied, François Charton, hat bereits 2019 untersucht, wie man das Transformer - Modell einsetzen kann, um Integralaufgaben zu lösen. Er lässt keine Details aus dem Blick, er schaut nicht, wie viel ein großes Modell schreiben kann, sondern ob es einen falschen Schritt macht.
Es gibt auch Hugh Leather, der die Deep Learning - Technologie mit Compilern kombiniert. Er ist nicht im herkömmlichen Sinne ein Mathematiker, aber er hat eine tiefe Erfahrung in der Darstellung komplexer Logik mit Code.
Sie alle haben Meta, Google und andere große Unternehmen verlassen und einen stabileren Forschungsweg aufgegeben.
Carina bietet nicht nur eine Stelle an, sondern eine Vision: Mit KI verifizierbare mathematische Ergebnisse zu erzielen, wobei jeder Schritt klar und jede Schlussfolgerung haltbar sein soll.
Und diese Vision hat nicht nur KI - Forscher aus der Branche angelockt.
Anfang Dezember 2025 hat auch der 57 - Jahre - alte Mathematiker Ken Ono seinen unbefristeten Lehrstuhl an der University of Virginia aufgegeben und sich vollzeit bei Axiom engagiert.
Er war einst Carinas Lehrer, hat mehrere Mathematikolympiade - Forschungsprojekte geleitet, ist ein Experte in der Ramanujan - Theorie und war sogar in einer Superbowl - Werbung. Er hat die Zahlentheorie in die Populärkultur gebracht.
Er sagt, als reiner Mathematiker hat er selten die Gelegenheit gehabt, etwas zu tun, das die Welt verändern kann. Diesmal will er nicht zuschauen, wie es vorbeigeht. Er hat seine Familie nach Silicon Valley gebracht und ist das 15. Mitglied von Axiom geworden, mit der Position als Gründungsmathematiker.
Seine Aufgabe besteht nicht darin, Code zu schreiben, sondern Schwierigkeiten zu entwerfen und die Grenzen der Modellschlussfolgerung zu testen.
Carina sagt, dass diese Leute nicht wegen einer Hype - Welle hierher gekommen sind, sondern weil sie etwas tun wollen, das wirklich wertvoll ist.
"Wir entwickeln nicht ein Produkt, sondern definieren einen neuen Standard: Jede Formel kann überprüft werden, jeder Schlussfolgerungsprozess kann nachvollzogen werden. Die KI zeigt nicht nur eine Antwort, sondern den gesamten Denkprozess."
Das ist, was diese 17 Leute derzeit tun.
Abschnitt 4 | Es geht nicht darum, Aufgaben zu lösen, sondern die KI zu lehren, Fragen zu stellen
Die Definition eines neuen Standards ist nur Carinas erster Schritt.
Was sie wirklich will, ist, dass die KI lernt, die Probleme selbst zu entdecken.
Zurzeit forschen sie an einem berühmten ungelösten Problem in der Mathematik: der Collatz - Vermutung. Dieses Problem ist so einfach wie ein Kinderspiel, aber es hat Forscher seit Jahrzehnten gefesselt.
Die Forscher von Axiom haben das Transformer - Modell eingesetzt, um dieses Problem zu lernen. Das Modell konnte keinen Beweis direkt geben, aber es hat eine andere Fähigkeit gezeigt:
Bei der Vorhersage der Collatz - Sequenz hat es eine Genauigkeit von 99,8 % für Zahlen im Billionenbereich erreicht.
Was noch wichtiger ist, kann man genau erklären, warum es fehlgeschlagen ist und wo der Fehler liegt. Hinter diesen Fehlern gibt es eine klare Regel, nicht zufällige Illusionen.
Was bedeutet das?
Es bedeutet, dass die KI nicht einfach Antworten auswendig lernt, sondern mathematisches Denken lernt.
Nach Carinas Meinung trainieren sie die KI nicht, um bekannte Antworten zu finden, sondern um wie ein echter Mathematiker zu denken und zu forschen.
Die Forscherung, die sie erwähnt, gliedert sich hauptsächlich in drei Phasen:
Erster Schritt: Die Theoreme in einer formalen Sprache ausdrücken und die bestehenden logischen Strukturen imitieren.
Zweiter Schritt: Verschiedene Lösungen für alte Probleme überprüfen und neue Beweiswege vorschlagen.
Dritter Schritt: Neue Vermutungen aufstellen, bisher nie dagewesene Probleme kreieren und mathematische Beweise liefern.
Der gesamte Prozess ist nicht wie ein zufälliges Gespräch mit ChatGPT, sondern eine geregelte Exploration im Beweisraum, ständiges Ausprobieren, bis man einen neuen Weg findet.
Warum ist diese Exploration so wichtig?
Weil die Mathematik die strengste Sprache der Menschheit ist und auch die zugrunde liegende Logik des realen Weltablaufs. Jeder mathematische Durchbruch kann in diesen Bereichen zu einem Sprung führen.
Carina glaubt, dass die mathematische Forschung früher mit einem Fortschritt alle zehn Jahre vorangeschritten ist, jetzt kann die KI diesen Zyklus auf einige Monate verkürzen.
Was ein Künstlicher Intelligenz - Mathematiker in Zukunft tun kann, ist nicht nur, Aufgaben zu lösen, sondern auch, zusammen mit Menschen die Probleme selbst neu zu definieren.
Dies ist nicht nur ein Problem im mathematischen Bereich. Sowohl in der Kryptographie, der Chip - Architektur als auch in der physikalischen Modellierung hängt alles von mathematischen Prinzipien ab