Spezialisiert auf die Bekämpfung von AI-Lügen: Das Unternehmen einer 25-jährigen Geniesfrau hat einen Schätzwert von über zehn Milliarden.

Hong Letong, 25, ist kürzlich in Silicon Valley berühmt geworden.

Dieses Mädchen aus Guangdong absolvierte mit 17 Jahren das MIT, absolvierte in drei Jahren einen Doppelabschluss in Mathematik und Physik und absolvierte anschließend ein Fortgeschrittenenstudium an der Stanford University.

Nach der in Silicon Valley am besten bekannten Erzählweise ist sie das Musterbeispiel für ein "geniales junges Mädchen, das ein Unternehmen gründet".

Was Hong Letong aber wirklich in Erinnerung lässt, ist nicht ihr Lebenslauf, sondern die Tatsache, dass die Dinge, die sie tut, so gegen die Intuition gehen.

Während die gesamte KI-Branche nach größeren Modellen, stärkerer Generierungsfähigkeit und menschlicherer Ausdrucksweise strebt, hat sie sich stattdessen für etwas entschieden, das am wenigsten sexy und am schwierigsten zu monetarisieren ist: die mathematische Validierung von KI.

Ihr gegründetes Unternehmen heißt Axiom. Es ist weniger als zwei Jahre alt, hat nur etwa 20 Mitarbeiter und hat kürzlich 200 Millionen US-Dollar in der Serie A-Rundung an Kapital angezogen. Der Unternehmenswert nach der Finanzierung beträgt stolze 1,6 Milliarden US-Dollar, was in chinesische Yuan umgerechnet über 11 Milliarden Yuan entspricht.

Axiom entwickelt keine Chatbots, keine Text-zu-Bild-Generatoren und folgt auch nicht der Hype um die großen Sprachmodelle. Stattdessen setzt es auf "formale Verifikation".

Einfach ausgedrückt, will man mit Mathematik und Logik sicherstellen, dass jeder Schritt der KI-Logik überprüfbar, beweisbar und nachvollziehbar ist.

Dies klingt sehr speziell, aber es zielt auf die größte Schwachstelle der großen Modelle ab - die Halluzination.

Das größte Problem der heutigen KI ist nicht, dass sie nicht stark genug ist, sondern dass sie nicht zuverlässig genug ist. Sie kann Antworten geben, die richtig klingen, und manchmal sogar die richtigen Lösungen finden, aber man kann nicht feststellen, ob sie die Lösung wirklich berechnet hat oder ob sie einfach "geraten" hat. Was Axiom tun will, ist, diesen unklaren Zustand in einen überprüfbaren, deterministischen Prozess zu verwandeln.

Deshalb, als Hong Letong mit dieser Idee auf die Suche nach Kapital ging, stieß sie nicht auf Beifall, sondern auf eine sehr realistische Frage: "Wie kann man mit Mathematik Geld verdienen?"

01 Die geniale junge Frau, die der Herausforderung entgegentritt

Hong Letongs Büro befindet sich an der University Avenue in Palo Alto in Silicon Valley, nur eine halbstündige Fußmarschdistanz von der Stanford University entfernt. Die Stanford war der Ausgangspunkt ihrer Doktorarbeit, aber bevor sie ihren Abschluss gemacht hatte, gründete sie ein Unternehmen.

Tatsächlich hatte Hong Letong bereits während ihrer Doktorarbeit ein Unternehmen gegründet. Das Unternehmen heißt Axiom, ein Name, der aus dem mathematischen Begriff "Axiom" stammt. "Ich möchte von Axiomen ausgehend einen Superintelligenz-Inferenzrechner schaffen, der sich selbst verbessern kann", sagte sie.

Eine 24-jährige Doktorandin ohne Geld, ohne Team und ohne Produkt gewann mit einer Idee 9,6 Millionen US-Dollar an Saatkapital.

Warum?

Die bestehenden großen Modelle sind im Wesentlichen probabilistische schwarze Kästen. Sie lernen Muster aus riesigen Datenmengen und geben dann auf der Grundlage statistischer Regeln Antworten. Der Inferenzprozess kann nicht quantifiziert werden, weshalb sie manchmal Unsinn erzählen und Fehler machen.

Was Hong Letong tun will, ist, mit mathematischen Axiomen und formaler Verifikation sicherzustellen, dass jeder Schritt der KI-Logik beweisbar ist und dass das System direkt auf Märkte wie Finanzwesen, Militär, Chip- und Autonomes Fahren zugeschnitten werden kann, die eine sehr hohe Zuverlässigkeit erfordern.

Das, was sie tut, trifft offensichtlich auf das größte Problem der KI zu: die Lösung der Probleme mit Halluzinationen und Zuverlässigkeit.

Darüber hinaus investieren Früheinvestoren in Menschen, und sie selbst ist ein echtes interdisziplinäres Genie.

Hong Letong hat schon als Kind bemerkenswerte mathematische Begabung gezeigt. Sie wurde 2001 in der Tianhe-Bezirk von Guangzhou geboren und besuchte die High School der South China Normal University. In der 10. Klasse qualifizierte sie sich für die nationale Mathematik-Olympiade und gewann in der Hua Luogeng-Wettbewerbsrunde und der nationalen Mathematikwettbewerbsrunde für High School-Schüler zahlreiche Preise.

Es war während der Olympiade-Trainings, dass sie sich für die forschende Mathematik interessierte.

2018 wurde sie mit 17 Jahren in das MIT aufgenommen und absolvierte in drei Jahren einen Doppelabschluss in Mathematik und Physik. Sie veröffentlichte neun wissenschaftliche Artikel und gewann unter anderem den Alice T. Schafer-Mathematikpreis, den höchsten Preis für weibliche Mathematikerinnen in den USA.

Danach erhielt sie ein Rhodes-Stipendium von der Universität Oxford. Anstatt sich weiter auf die Mathematik zu konzentrieren, wechselte sie auf die Neurowissenschaften, um "ein kognitives System zu entwickeln, das über wissenschaftliche Disziplinen hinweg greift".

Basierend auf diesem Ziel führte sie gleichzeitig an der Gatsby Computational Neuroscience Unit der University College London Forschungen in der Deep Learning-Technologie durch. Diese Einheit wurde von Geoffrey Hinton, dem "Vater des Deep Learning", mitbegründet. Es war auch während dieser Zeit, dass sie erstmals in die KI-Branche eintrat und viele der neuesten Themen kennenlernte. Anschließend wechselte sie an die Stanford University, um einen Doppel-Doktorandenabschluss in Mathematik und Recht zu erwerben.

Im Jahr 2024 wurde bekannt, dass ChatGPT o3 beim Mathematiktest "geschummelt" haben könnte, was die Weltöffentlichkeit in Aufruhr versetzte.

Hong Letong, eine Doktorandin in Mathematik an der Stanford University, äußerte sich auch in den sozialen Medien: "Es ist sehr wahrscheinlich, dass das große Modell von OpenAI bei den Mathematiktests gut abgeschnitten hat, weil die Testfragen in den Trainingsdaten vorab bekannt waren. In einigen Tests erreichte das große Modell zwar eine Genauigkeit von 96 %, aber sobald der Inferenzprozess gezeigt wurde, sank die Erfolgsrate auf 5 %."

Angesichts der Branchenprobleme trat eine Sprache namens Lean in ihr Blickfeld und bot ihr eine Geschäftsmöglichkeit.

Im Gegensatz zu natürlichen Sprachen ist Lean eine sehr besondere, selbstverifizierende mathematische Programmiersprache. Hong Letong gab ein Beispiel: "Wenn ich einen mathematischen Beweis in Englisch schreibe, kann ich nicht wissen, ob ein 5.000-Zeilen-Beweis richtig ist. Ich muss einen hochqualifizierten Experten bitten, ihn zu überprüfen. Aber Lean ist selbstverifizierend. Wenn es funktioniert, ist es richtig."

Die Logik von Lean besteht darin, natürliche Sprache oder nicht-formale Verifikation in eine maschinenüberprüfbare formale Verifikation umzuwandeln.

Was ist nun formale Verifikation?

Bei normalen KI-Systemen kann man nur anhand der Antworten beurteilen, ob das System die Frage versteht, aber man weiß nicht, ob es geraten hat.

Formale Verifikation erfordert, dass jeder Schritt in eine maschinenüberprüfbare logische Kette geschrieben wird. Wenn ein Schritt fehlt, unklar ist oder man sich bei einem Schritt "zusammenreißt", wird der Beweis nicht akzeptiert.

Der Grund, warum formale Verifikation die Halluzinationen von großen Modellen bekämpfen kann, ist, dass formale Verifikation unabhängig von der Antwort ist. Wenn die Schlussfolgerung schrittweise legal aus den Prämissen abgeleitet wird, ist die Antwort richtig, wodurch Halluzinationen des Modells vermieden werden.

Deshalb lässt Axiom das große Modell für Vermutungen und Suche zuständig sein und Lean für die Überprüfung und Entscheidung. Wenn Lean feststellt, dass der Prozess falsch ist, wird der Vorgang zurückgesetzt und korrigiert.

Doch dies ist eindeutig ein enger Weg. Wie speziell ist dieser Weg? Im gesamten KI-Landschaft ist formale Verifikation fast an der Peripherie, und die Anzahl der kommerziellen Akteure weltweit lässt sich an den Fingern einer Hand abzählen.

Offensichtlich hat sie nicht deshalb für formale Verifikation entschieden, weil es der nächste Hype sein würde, sondern weil ihre Definition von "Schwierigkeit" von der anderer Menschen abweicht.

"Der Mathematik-Olympiade ist wie ein ständiger Dopamin-Schub, während die forschende Mathematik wie ein Kopf an die Wand rennen ist, voller Schmerz und Frustration. Ich mag diese Herausforderung wirklich", erklärte sie einmal, warum sie sich so für Mathematik begeistert.

Es ist diese in ihrem Blut stehende Lust nach Herausforderungen, die sie nicht im Komfortbereich der akademischen Forschung bleiben lässt, sondern sie ermutigt, in einem breiteren Feld die harten Nüsse in der KI-Branche zu knacken.

Im späten Herbst 2024 sprach Hong Letong in einem Café in der Nähe der Stanford University mehrere Stunden lang mit Shubho Sengupta, dem damaligen Leiter der Meta AI-Forschung, über ein einziges Thema: Kann KI wirklich mathematische Inferenz lernen?

Die beiden waren sich einig, einer gab sein Studium auf, der andere kündigte seine Stelle, und beide gründeten zusammen ein Unternehmen.

02 Eine Legion von "Graswurzel"-Ingenieuren

Axiom hat nur etwa 20 Mitarbeiter. Hong Letong beschreibt die Stimmung des Teams mit einem Wort: "Graswurzel-Ingenieurgeist".

Tatsächlich sind die Mitglieder dieses Teams gar nicht so "graswurzelig", sondern haben sogar eine beeindruckende Hintergrund.

Der erste Mitarbeiter von Axiom ist Shubho Sengupta, ein ehemaliger Mitarbeiter von Meta, mit dem sie im Café mehrere Stunden lang gesprochen hat. Heute ist er der CTO des Unternehmens.

Der Kernwissenschaftler François Charton ist ein Pionier bei der Einführung der Transformer-Architektur in das Gebiet der mathematischen Inferenz. Sein Job besteht darin, mathematische Formeln als eine Art "Sprache" in den Transformer einzugeben und zu testen, ob der Transformer Mathematik wie einen Satz übersetzen kann.

Etwa die Hälfte der anderen Mitglieder stammt aus Meta AI, die andere Hälfte besteht aus weltbekannten Mathematikern und Pionieren der formalen Verifikation.

Der am meisten aufsehenerregende Mitarbeiter ist der 57-jährige Mathematikgigant Ken Ono.

Er ist ein führender Wissenschaftler auf dem Gebiet der Modulformen, ehemaliger Vizepräsident der American Mathematical Society und hat unter anderem den Guggenheim-Preis und den Sloan-Preis erhalten. Zehn seiner Schüler haben den Morgan-Preis gewonnen. Er hat auch die US-Olympiaschwimmmannschaft bei der Datenanalyse unterstützt und als Berater für den Film "The Man Who Knew Infinity" gewirkt.

Dieser Professor an der University of Virginia kam mit Hong Letong an der Massachusetts Institute of Technology zusammen. Damals war Hong Letong ein erstes Semesterstudentin und beteiligte sich an seinem Zahlentheorie-Projekt. Die Lehrer-Schüler-Beziehung besteht bis heute, aber ihre Rollen haben sich geändert. Ende 2025 kündigte Ken Ono seinen Lehrposten und trat als der 15. Mitarbeiter vollzeitlich bei Axiom ein.

Warum war Ken Ono, der Einladungen von Google und Meta abgelehnt hatte, bereit, für eine 24-jährige Studentin zu arbeiten?

"Wenn meine Vermutungen von einer Maschine innerhalb von drei Tagen auf zehn Dimensionen erweitert werden können, bin ich bereit, ein 'Annotator' zu sein", sagte Ken Ono einmal öffentlich. Er entschied sich, für seine ehemalige Schülerin zu arbeiten, nicht nur weil Hong Letong einen Vertrag mit "keiner Lehre, keinem administrativen Aufwand und 100 % Forschung" anbot, sondern vor allem, weil ihn die "Dimensionenreduktion" durch KI aufregte.

Eine Gruppe von Spitzenwissenschaftlern und ehemaligen Meta-Mitarbeitern - wo ist da der "Graswurzel"-Charakter?

Hong Letong erklärt, dass "Graswurzel" eine Haltung des ständigen Lernens und eine zähe Perspektive repräsentiert. Auf dem Weg des Unternehmertums müssen selbst erfahrene "Experten" von vorne anfangen und sich ständig weiterentwickeln.

Sie selbst bevorzugt es nicht, ein "Elite-Mitglied" zu sein, sondern ein "Graswurzel", ein "Niemand". So kann man am schnellsten lernen.

Sie selbst ist auch eine praktizierende Person des "Graswurzel-Geistes". Als man sie fragte, wie sie ihr Team leite, sagte Hong Letong: "Ich mag das Wort 'leiten' eigentlich nicht. Ich möchte ein 'Individual contributor' sein, und jeder sollte es auch sein. Dies ist eine Gruppe von Menschen mit gleichen Interessen, die zusammenarbeiten."

"Wir haben Axiom gegründet, um die Zeit zu verkürzen, in der Neugierde in Wahrheit umgewandelt wird", sagte Hong Letong. In Silicon Valley, getrieben von Kapital, ist diese Reinheit vielleicht für Spitzenforscher attraktiver als ein lukratives Jobangebot.

Dieses Team von weniger als 20 Personen hat in weniger als einem Jahr nach seiner Gründung ein überraschendes Ergebnis erzielt.

Am 3. Dezember 2025 kündigte Axiom an, dass sein Kernsystem AxiomProver ohne menschliche Intervention zwei von Paul Erdős gestellte Probleme gelöst hatte, die die mathematische Welt seit Jahrzehnten beschäftigten.

Am gleichen Tag erhielt Hong Letong die Nachricht, dass sie in die "Forbes 30 Under 30"-Liste aufgenommen wurde.

Im gleichen Monat erreichte AxiomProver in der Putnam-Mathematikwettbewerbsrunde volle Punktzahl, alle 12 Aufgaben richtig gelöst. Der Putnam-Wettbewerb ist der renommierteste Mathematikwettbewerb für Studenten in Nordamerika. Die Medianpunktzahl ist oft Null, und in den letzten fast 100 Jahren haben nur fünf menschliche Teilnehmer volle Punktzahl erreicht.

Axiom hat weiter bestätigt, dass die Konstruktion einer zuverlässigen, überprüfbaren und halluzinationsfreien KI durch formale Verifikation eine klare und wichtige Richtung für die Branche ist, und AxiomProver hat auf diesem Weg ein reproduzierbares und hochschwieriges Beispiel geliefert.

03 Der Wettlauf wird heiß, aber die Herausforderungen beginnen erst

Betrachtet man die Branchenentwicklung, hat Hong Letong genau den richtigen Zeitpunkt getroffen.

Ende 2024 veröffentlichten mehrere Institutionen, darunter Meta FAIR und die Stanford University, eine Positionspapier namens "Formal Mathematical Reasoning: A New Frontier in AI".

Das Papier kommt zu dem Schluss, dass die bisherige KI-Mathematik darin bestand, das Modell mit vielen Mathematikaufgaben zu füttern und dann Antworten auszugeben. Dies führt dazu, dass die Daten kontaminiert werden, der Prozess erfunden wird, die KI nicht selbst entscheiden kann, ob die Antwort richtig ist, und der Prozess schwer reproduzierbar ist.

Offensichtlich ist dies der falsche Weg. Nehmen wir das Multiplikationstafel als Beispiel. Wenn es dort steht, dass 2 * 3 = 6, dann kann man auch verstehen, dass 3 * 2 = 6. Dieser Prozess heißt Reproduzierbarkeit.

Das Papier plädiert dafür, dass im nächsten Schritt Be