Axiom: KI-Mathematiker erzielt perfektes Ergebnis bei Putnam-Wettbewerb – Series A mit 1,6 Mrd. $ bewertet
Die 24-jährige Gründerin Carina Hong schließt 200-Millionen-Dollar-Finanzierungsrunde ab und baut ein Team aus Meta-KI-Veteranen und renommierten Mathematikern wie Ken Ono auf
Sieben Monate nach der Gründung von Axiom hat Carina Hong eine Series-A-Finanzierung über 200 Millionen Dollar bei einer Bewertung von 1,6 Milliarden Dollar abgeschlossen. Damit festigt sie ihre Position als jüngste Gründerin in der aktuellen Welle von „Neo Labs“, die das Silicon Valley erfasst. Das AxiomProver-System des Unternehmens erzielte im Dezember 2025 das sechste perfekte Ergebnis in der 98-jährigen Geschichte des Putnam Mathematics Competition – ein Wendepunkt für KI-gestützte mathematische Beweisführung. Besonders bemerkenswert ist die Art der Leistung: Während menschliche Lösungen oft auf geometrischer Intuition beruhen, generierte AxiomProver tausende Zeilen Lean-Code durch Brute-Force-Enumeration – ein grundlegend anderer Ansatz, der dennoch zu korrekten Beweisen führte.
Die Finanzierung markiert eine deutliche Steigerung gegenüber der Seed-Runde von Axiom, die nur wenige Monate zuvor mit 64 Millionen Dollar bei einer Bewertung von 300 Millionen Dollar abgeschlossen wurde. Hong beschreibt den Fundraising-Prozess der Seed-Runde eher als anstrengend denn als schwierig: „Man sagt immer wieder dasselbe. Man bekommt immer wieder dieselben Fragen. Ich könnte es aufnehmen und euch allen schicken, oder?“ Die Runde war von einem intensiven Bieterwettstreit geprägt, der das ursprüngliche Angebot verdreifachte. Howard Morgan von B Capital – Mitgründer von Renaissance Technologies an der Seite von Jim Simons sowie Mitgründer von First Round Capital – führte die Runde schließlich an. Hong erinnert sich, dass Morgan mehr Optimismus für das Geschäftsmodell zeigte, als sie selbst hatte, und sie direkt auf potenzielle Anwendungen hinwies, die sie noch gar nicht vollständig artikuliert hatte.
Von Verve Coffee zu formalen Beweisen
Die Entstehungsgeschichte ist für ein Silicon-Valley-Einhorn ausgesprochen ungewöhnlich. Hong lernte ihren Mitgründer und CTO Shubho Sengupta bei Verve Coffee in Palo Alto kennen, wo beide Stammgäste waren. Sengupta, ein Veteran von Meta AI und einer der frühen Entwickler von CUDA im KI-Labor von Baidu im Silicon Valley (2015–2016), arbeitete an der Seite von Persönlichkeiten wie Dario Amodei (heute Gründer von Anthropic). Ihre Beziehung begann nicht mit einem Pitch, sondern mit achtzehn Monaten voller Gespräche über die Geschichte der Wissenschaft. Hong war zu dieser Zeit Doktorandin für Jura und Mathematik in Stanford, las Rechtsfälle und beobachtete Hunde im Innenhof; Sengupta war ein erfahrener Forscher auf der Suche nach intellektuellem Austausch außerhalb der Mauern von Meta.
Der Wendepunkt kam während eines Kurses zum Verfassungsrecht, als Hong erkannte: Wenn eine KI die präzise Sprache der Verfassungsinterpretation analysieren kann – ein textbasierter Ansatz, der strikte definitorische Strenge erfordert –, dann sollte sie erst recht in der Lage sein, mathematische Beweise zu handhaben. Sie verfolgte seit 2020 die Arbeit ihres Freundes Kenny Luo, der mathematische Grundlagen für das Grundstudium in Lean, der Sprache zur Beweisverifikation, formalisierte. „Wenn KI Jura kann, dann deshalb, weil sie etwas Strukturierteres sieht“, erklärt Hong. „Mathematik ist eine strukturellere Präsentation.“ Im September 2024 beschloss sie, ein Unternehmen zu gründen, obwohl sie zwei Monate damit verbrachte, sich selbst davon abzubringen. „Ich glaube eigentlich, wenn ich Studentin wäre, würde ich niemals das Studium abbrechen und zu Y Combinator gehen. Ich fühle mich wie die unwahrscheinlichste Unternehmerin, die ein Geschäft startet.“
Der Brute-Force-Spieler baut ein System
Hong Selbsteinschätzung, keine „talentierte Spielerin“ zu sein, sondern jemand, der durch schiere Beharrlichkeit Erfolge erzielt, durchzieht ihren Ansatz sowohl in der Mathematik als auch beim Firmenaufbau. Am MIT kämpfte sie mit euklidischen Geometrieproblemen, die bei Mathematikwettbewerben als „Must-have“-Aufgaben galten, und löste sie schließlich durch komplexe Zahlenmethoden, die zwei- bis dreimal länger dauerten als eine Lösung per geometrischer Intuition. „Normalerweise addiere ich einfach jeden Punkt und verwende dann diese Methode der komplexen Zahlen für jede Linie. Man muss einfach hart arbeiten, um Wunder zu vollbringen. Am Ende muss ich die geometrische Bedeutung dahinter gar nicht verstehen.“ Diese Erfahrung prägte ihre Überzeugung, dass KI gerade „Brute-Force“-Mathematikern am meisten nützen könnte: „Vielleicht geht es wirklich darum, wie viele Möglichkeiten ich aufzählen will? Wie viele Tage habe ich Zeit, um ein sehr standardmäßiges Argument zu verifizieren?“
Die technische Architektur spiegelt diese Philosophie wider. Axioms System kombiniert verschiedene Arten von KI: Reinforcement-Learning-Agenten für angewandte KI-Arbeiten, Teams für Codegenerierung und Compiler (darunter Kernmitglieder von Metas „CodeWorld“-Modell mit 32 Milliarden Parametern) sowie reine Mathematiker, die an Leans Mathlib arbeiten. Das Unternehmen vermied es bewusst, Mathematiker einzustellen, bis es fünfzehn Mitarbeiter erreichte, da der frühe Fokus auf technischen Herausforderungen liegen sollte und nicht auf mathematischer Intuition. Als sie schließlich Mathematiker an Bord holten, geschah dies mit einem spezifischen Ziel: Professor Ken Ono kam dazu, um gegnerische Benchmarks zu erstellen und das System ständig an seine Grenzen zu bringen, anstatt Erfolge nur zu feiern.
Hong unterscheidet zwischen dem Ansatz von Axiom und Wettbewerbern, die stark auf Monte Carlo Tree Search setzen, die Methode, die auch bei DeepMinds AlphaProof verwendet wird. „Wir halten das für zu teuer. Schauen wir mal, wie viel Geld wir haben. Wir glauben nicht, dass wir diesen Monte-Carlo-Baum machen können.“ Stattdessen erforschte das Team Sub-Agenten und fähigkeitsbasierte Ansätze und stellte unerwartete Synergien zwischen mathematischem Beweis und Code-Verifikation fest. Beim Verina-Benchmark für Code-Verifikation erzielte AxiomProver Ergebnisse, die „uns alle überrascht haben“, was zeigt, dass eine starke Fähigkeit zum Theorembeweis direkt in Fähigkeiten zur Code-Validierung übersetzt werden kann – eine entscheidende Erkenntnis für zukünftige Geschäftsanwendungen.
Ken Onos unerwartete E-Mail
Die Rekrutierung von Ken Ono, einem 57-jährigen, fest angestellten Professor an der University of Virginia und prominenten Zahlentheoretiker, erregte bei der Ankündigung große Aufmerksamkeit. Die Realität war jedoch organischer als dramatisch. Ono hatte Hong während eines REU-Programms (Research Experience for Undergraduates) betreut, als sie noch eine Studentin auf der Warteliste war; später arbeiteten sie an mehreren Publikationen zusammen. Im November 2024 schickte er eine E-Mail, in der er mitteilte, dass er in die Bay Area komme und er hoffe, sie sei nicht verärgert, falls er bei OpenAI oder DeepMind anfangen würde. Hongs Antwort kam sofort: „Ich sagte, du kannst zu mir kommen.“
Was Ono dazu bewog, Axiom gegenüber OpenAI zu bevorzugen, war der Fokus und die Kultur. „Er findet, unser Team ist mathematischer“, erklärt Hong. „Wenn man zu uns kommt, herrscht vielleicht mehr Atmosphäre der Mathematik. Die DNA und der Fokus dieses Unternehmens liegen auf der Mathematik, anstatt auf einer allgemeinen AGI, bei der Mathe nur ein Teil davon ist, vielleicht eher eine Marketingkomponente.“ Onos Rolle geht über die Forschung hinaus; Hong beschreibt ihn als jemanden mit der Persönlichkeit eines „Highschool-Basketballtrainers“ – unermüdlich optimistisch, teamorientiert und geschickt darin, andere glauben zu lassen, dass schwierige Ziele erreichbar sind. Seine Präsenz zieht zudem andere Mathematiker an, die der Rolle von KI in ihrem Fachgebiet gegenüber sonst skeptisch wären.
Die Frage, ob KI die Existenzgrundlage von Mathematikern bedroht, beantwortet das Axiom-Team differenziert. Ono und andere glauben zunehmend, dass Mathematiker, während die KI mehr Beweise übernimmt, „auf verschiedenen Abstraktionsebenen lernen“ werden. Sie werden sich auf höherwertige Fragen konzentrieren: Welche Probleme sind es wert, gelöst zu werden, und wie strukturiert man Theorien? Hong nutzt eine Analogie: Die Programmierung entwickelte sich von Lochkarten über Low-Level-Assembler zu Python und natürlicher Sprachprogrammierung. Die Mathematik könnte einen ähnlichen Weg einschlagen, bei dem Mathematiker auf immer abstrakteren Ebenen arbeiten, während die KI die mechanische Verifikation und sogar Teile der Beweisgenerierung übernimmt.
Die Krise der Mathe-Benchmarks und Forschungsherausforderungen
Axioms schneller Fortschritt schuf ein unerwartetes Problem: die Sättigung von Benchmarks. Das Team brachte „mini-f2f“ (Highschool-Niveau) in etwa zwei Monaten zur Sättigung, danach dasselbe mit Putnam. „Um ehrlich zu sein, mangelt es uns auf Forschungsebene an Benchmark-Sets, weil es in der mathematischen Forschung nicht viele davon gibt“, räumt Hong ein. Die berühmte FrontierMath-Challenge stellt andere Probleme – viele Fragen können nicht einmal in Lean formalisiert werden, da die erforderlichen Definitionen in Mathlib, der zentralen Mathematikbibliothek, nicht existieren. Hong versuchte, an dieser Challenge teilzunehmen, konnte die Probleme aber nicht in Lean konvertieren: „Die Frage beinhaltet viele Definitionen. Diese Definitionen sind in dieser Bibliothek überhaupt nicht vorhanden.“
Dies deutet auf eine tiefere technische Herausforderung hin, die Hong als potenziell schwieriger einstuft als den Beweis selbst: die Auto-Formalisierung, also die Umwandlung von Mathematik in natürlicher Sprache in formalen Lean-Code. „Wenn ich diese bereits entdeckte und aufgeschriebene menschliche Mathematik nehme und in formalisierte Daten umwandle, bekommt man weniger Anerkennung, als wenn man etwas beweist. Aber diese Technologie ist eigentlich schwieriger als der Beweis. Zumindest auf dem gleichen Schwierigkeitsgrad. Ich glaube sogar, es ist schwieriger.“ Der Prozess erfordert die Erstellung detaillierter Blaupausen – man nimmt ein 20-seitiges Papier und erweitert es auf 200 bis 500 Seiten granularer Beweisschritte, die dann formalisiert werden können. Terence Tao und andere haben dies für große Gemeinschaftsprojekte manuell getan, aber die Automatisierung bleibt ein ungelöstes Problem.
Die aktuellen technischen Prioritäten des Unternehmens liegen in der Skalierung der Inferenz durch Sub-Agenten, anstatt sich auf rechenintensive Baumsuche zu verlassen. Hong beschreibt einen „Aha-Moment“, als das Team Beweise von 40-Knoten-Bäumen auf 4.000-Knoten-Bäume skalierte und zeigte, dass „Lernen aus Erfahrung“ – jede Problemlösungs-Trajektorie als Trainingsdaten für den Kompetenzerwerb zu behandeln – im großen Maßstab funktionieren kann. Eine weitere entscheidende Erkenntnis betraf die Beziehung zwischen Mathematik und Code: „Es klingt sehr albern, Leuten zu sagen, dass KI-Arbeit der Vergangenheit gut in Mathe war, aber von Mathe zur Codegenerierung, von Mathe zur Chip-Verifikation für diesen Code – das sind offensichtliche Transformationen.“ Die Implikation ist, dass Axioms Kerntechnologie nicht nur Mathematik betrifft, sondern verifizierbares Denken, das auf jeden Bereich mit formalen Spezifikationen anwendbar ist.
Geschäftsmodell und die „Validation-First“-Strategie
Hong ist entwaffnend offen, was die Unsicherheit des Geschäftsmodells angeht. Während der Seed-Runde sagte sie Investoren: „Unser Geschäftsmodell ist nicht sehr sicher. Ich war selbst quantitative Händlerin. Ich weiß nicht, ob dieses Ding quantitativer Handel ist. Ich glaube vielleicht nicht. Ich sagte damals, dass dies als Geschäftsmodell nicht das endgültige Geschäftsmodell sein kann. Dies ist nur ein Beispiel dafür, dass eine KI, die besser in Mathematik ist, nützlich sein kann.“ Diese Offenheit spiegelt ihren Hintergrund wider – sie wäre fast zu Bridgewater Associates gegangen, bevor die Pandemie sie zum REU-Programm von Professor Ono umleitete. Quantitative Finanzen stellten eine klare Anwendung dar, aber Hong glaubt nicht, dass dies der Endzustand ist.
Das Unternehmen hat sich auf Validierung als ersten Markt festgelegt: Chip-Verifikation, Schaltungsverifikation und Code-Verifikation, wo formale Methoden derzeit auf teure, arbeitsintensive SMT-Solver und Tools wie Cadence Jasper angewiesen sind. Das automatisierte Reasoning-Team von Amazon verbrachte drei bis fünf Jahre damit, 260.000 Zeilen Code zu schreiben, um eine einzige Hypervisor-Speicherisolationskomponente zu verifizieren. „KI verbessert das Leben dieser Ingenieure nicht“, beobachtet Hong. „Aber in diesen Bereichen hat man eine bessere Preissetzungsmacht.“ Die Vision reicht bis in eine Zukunft, in der jeder Programmierer eine Funktion mit der Garantie anfordern kann, dass sie korrekt funktioniert – ohne Testfälle –, obwohl Hong einräumt, dass dies noch „5–10 Jahre“ entfernt ist und die Lösung des Spezifikationsproblems erfordert, das nach wie vor extrem schwierig ist.
Trotz des Fokus auf Validierung hält Hong daran fest, dass KI für Mathematik im Grunde ein „Moonshot“ mit binären Ergebnissen ist. „Entweder die Mondlandung ist erfolgreich oder sie scheitert. Ja, die Mondlandung war erfolgreich, die Mondlandung ist gescheitert“, sagt sie und vergleicht Axiom explizit mit SpaceX. „Es gibt keine Möglichkeit dazwischen.“ Dies erzeugt Spannungen zwischen langfristigen Forschungsambitionen und dem kurzfristigen Druck zur Umsetzung. Die hohen Erwartungen der Series A könnten das Unternehmen zu einer inkrementellen Kommerzialisierung drängen, aber Hong glaubt, dass die DNA des Teams etwas anderes verlangt: „Wenn wir nur zu sehr auf Gewinnstreben und Kommerzialisierung setzen, werden wir tatsächlich aus dem Gleichgewicht geraten. Wir können uns unsere Konkurrenzunternehmen ansehen. In den frühen Tagen sprachen sie mehr über wissenschaftliche Ambitionen. Wir halten uns für ideale Realisten und realistische Idealisten. Beides ist gut.“
Wettbewerb, Ressourcen und das Neo-Lab-Phänomen
Axiom befindet sich in einer eigenartigen Wettbewerbsposition. Der Hauptkonkurrent, zwei Jahre früher gegründet und mit fünfmal mehr Startkapital ausgestattet, erreichte nach zwei Jahren Arbeit IMO-Niveau (Lösung von 5 von 6 Problemen). Axiom erreichte die Putnam-Perfektion in vier Monaten. Dennoch operiert das Unternehmen mit nur 30 Personen im Vergleich zu den 50–75 des Konkurrenten und hat laut Hong unzureichendes Kapital für ihre Ambitionen aufgenommen: „Jeder denkt, wir hätten zu wenig aufgenommen. Wir haben für unsere Seed-Runde nicht genug Kapital aufgenommen.“ Die Ressourcenbeschränkungen erzwangen strategische Entscheidungen – kein Pre-Training, Fokus auf Post-Training und Systemdesign sowie aggressives Anwerben von Talenten, die bereit sind, Startup-Kompensation statt der Millionen-Dollar-Pakete etablierter KI-Labore zu akzeptieren.
Die Herausforderung bei der Rekrutierung ist existenziell. Anfang 2025 hatten die meisten KI-Talente sechs konkurrierende Angebote, und Hong fehlte die Hebelwirkung: „Ich habe 6 Angebote auf dem Tisch. Ich wurde zu der Person, die tanzen muss. Vielleicht kann man nicht Peter Thiel sein.“ Sie beschreibt Rekrutierungsentscheidungen als den schmerzhaftesten Aspekt des Unternehmertums, Situationen, in denen „man vielleicht denkt, es gibt einen Konflikt zwischen Menschen und Dingen, aber eigentlich ist man selbst nicht gut genug.“ Die Bottom-up-Kultur des Unternehmens – geerbt von den Facebook-Veteranen, die den Großteil des frühen Teams bilden – hilft dabei, Talente anzuziehen, die Forschungsfreiheit statt Top-down-Vorgaben wollen. Hong kultiviert dies bewusst: „Wenn man wissen will, was das bedeutet, kann man sich ein LLM nehmen, ihm einige Daten geben. Ich glaube, unsere National Foundation muss Forschungsgelder für reine Mathematik bereitstellen, denn Mathematik ist ein Ökosystem.“
Die breitere Welle der „Neo Labs“ liefert den Kontext für Axioms Entstehung. Hong sieht darin eine Reaktion auf strukturelle Ineffizienzen in großen Organisationen: „Wettbewerb, der zu Mittelmäßigkeit führt, hat zur Folge, dass man keine langfristigen Ideen mehr hat. Man muss rausgehen und es selbst machen, ein Neo Lab gründen. Die Geburt der Neo Labs liegt in Neugier und Kreativität begründet – das ist unser grundlegendes menschliches Bedürfnis.“ Sie glaubt, dass große Frontier-Labore vor einer grundlegenden Spannung stehen: Sie werden weiterhin allgemeine Fähigkeiten vorantreiben, während spezialisierte Startups bei vertikalen Problemen schneller vorankommen können. OpenAIs Ansatz für KI in der Mathematik konzentriert sich auf informelle Beweise in natürlicher Sprache; DeepMind hat mehrere konkurrierende Teams, die an formalen und informellen Ansätzen arbeiten; Anthropic nutzt mathematisches Denken, um allgemeine Denkfähigkeiten zu verbessern, anstatt es zu einem Kernfokus zu machen.
Die technische Grenze: Vom Beweis zur Vermutung
Hong artikuliert eine Taxonomie der Fähigkeiten von KI für Mathematik, die über den Beweis hinausgeht. „Man braucht einen sehr guten Prover. Man braucht ein sehr gutes Vermutungssystem, das mathematische Fragen stellen kann. Die Belohnung für diese KI ist, wenn ich diesen Prover nehmen kann, um das Belohnungssignal für diese Vermutung zu erzeugen.“ Das Vermutungsproblem bleibt weitgehend ungelöst, da Vermutungen im Gegensatz zu Beweisen – die eine binäre Verifikation haben (bewiesen oder nicht) – keine klaren Belohnungssignale aufweisen. Woher weiß eine KI, ob ihre Vermutung interessant, wichtig oder sinnvoll ist, im Gegensatz zu trivial? Der aktuelle Stand der Technik nutzt grobe Heuristiken wie die Beweislänge im Verhältnis zur Aussagelänge als „Eleganzfilter“, aber das funktioniert über dem Niveau der Highschool-Mathematik nicht mehr.
Eine zweite große Herausforderung ist das „Library Learning“: Die KI soll nicht nur Theoreme innerhalb bestehender Definitionen beweisen, sondern neue Definitionen erstellen und Theorien aufbauen. „Die Maschine soll eine Bibliothek aus der Definition aufbauen, einschließlich der Theoreme darüber, einschließlich des Beweisens dieser Theoreme, und dann neue Theoreme ableiten und weitere Definitionen hinzufügen. Dieser Prozess ist ein Prozess der architektonischen Theorie. Das ist ziemlich schwierig.“ Die Schwierigkeit liegt in der Verifikation – wie kann man sicherstellen, dass eine maschinengenerierte Definition keine logischen Inkonsistenzen erzeugt, die sich erst hunderte Schritte später als Paradoxien manifestieren? In einer hypothetischen Zukunft, in der die gesamte menschliche Mathematik in Lean formalisiert ist, wird dies entscheidend: „Wenn diese Definition eine ist, die ein Mensch nicht hat, eine Definition, die nie geschrieben wurde, wie kann ich garantieren, dass diese Definitionen dieses Systems nicht miteinander in Konflikt stehen?“
Die Beziehung zwischen formalem Beweis in Lean und dem Denken in natürlicher Sprache erzeugt faszinierende technische Spannungen. Hong formuliert es als „Mathe ist Code und Code ist Mathe“ durch die Curry-Howard-Korrespondenz, bei der jeder mathematische Beweis in ein Computerprogramm umgewandelt werden kann. Aber diese Übersetzung ist nicht symmetrisch – Englisch in Lean zu konvertieren ist weitaus schwieriger als Lean in Englisch, weil das Modell weitaus mehr englische Tokens gesehen hat. Axiom nutzt Zykluskonsistenz (Übersetzung in Lean, Rückübersetzung, Prüfung auf Unterschiede), um Konvertierungen zu validieren. Hong glaubt, dass Sprachmodelle gute Vermutungen durch ihre Fähigkeit erzeugen können, Grenzen zu überschreiten, aber die Verifikation muss im formalen Raum stattfinden. „Sprache kann eine gute Vermutung machen. Dann ist Generierung bis zu einem gewissen Grad Generierung, dann verifizieren – diese beiden gehen Hand in Hand.“
Die Identitätskrise des Mathematikers
Hongs persönliche Reise spiegelt breitere Fragen darüber wider, was es bedeutet, in einem Zeitalter KI-gestützter Beweise Mathematiker zu sein. Am MIT fühlte sie sich wie „die Dümmste im ganzen Fachbereich“, umgeben von IMO-Goldmedaillengewinnern, deren Nachrichten sie seit ihrer Kindheit verfolgt hatte. Ihre Reaktion war keine Verzweiflung, sondern Akzeptanz: „Meine Erwartung ist, dass ich die Dümmste bin, also passe ich mich eigentlich sehr gut an. Ich fühle mich jeden Tag glücklich, dass ich mit diesen Leuten sprechen, gemeinsam Kurse besuchen und Hausaufgaben machen kann.“ Diese Einordnung – dankbare Auszubildende statt konkurrierendes Genie – prägte ihren Ansatz sowohl für die Mathematik als auch für den Firmenaufbau.
Die Frage, ob sie als Mathematikerin in Erinnerung bleiben möchte, erhält eine überraschend philosophische Antwort. „Früher dachte ich, das sei wichtig. Ich habe früher manchmal geweint. Ich bin immer noch ein sehr emotionaler Mensch. Dann fühlte ich später: Eigentlich möchte ich eine Auszubildende sein. Ich möchte einfach in so viele intellektuelle Bereiche wie möglich eintauchen und so viel wie möglich lernen.“ Sie beschreibt den Sprung von Mathe zu Physik (um zu heilen, dass sie „in der Highschool sehr schlecht in Physik war“), zu Neurowissenschaften, zu KI, zu quantitativem Handel und zu Jura. Jeder Übergang war von Neugier auf unbekannte Bereiche getrieben. „Das könnte eine gute Sache sein – wie kann ich es zulassen, dass ein Auszubildender, ein Unternehmer-Lehrling, nicht stirbt? 99 % der Startups werden sterben. Warum sterbe ich jetzt einfach nicht?“
Die Frage nach einem Abendessen mit einem Mathematiker ruft eine bezeichnende Antwort hervor: Erdős, weil „die Beschreibungen, die er dir gab, schließlich Kombinatorik sind, man kann verstehen, was man zum Abendessen auf dem Tisch hat.“ Erdős repräsentiert Mathematik als soziale Praxis, der reisende Mitarbeiter mit hunderten Co-Autoren und einer eigenartigen Persönlichkeit. Hong kontrastiert dies mit Grothendieck, dessen Abendessen „von großer Bedeutung“ wäre, dessen abstrakte algebraische Geometrie aber bei jemandem ohne das erforderliche Hintergrundwissen verschwendet wäre. Die Implikation ist, dass mathematischer Wert nicht nur in Theoremen existiert, sondern in der Gemeinschaft und der Kultur, die sie umgibt – etwas, das KI ergänzen, aber nicht ersetzen kann.
Die Sucht nach dem Leiden und das Pendel der Geschichte
Auf die Frage nach ihrem Selbstbelohnungsmechanismus beschreibt Hong eine Verschiebung: von der Energie, die sie aus kleinen Teams und Kameradschaft zog, hin zu der Energie, die sie aus der Arbeit selbst bezieht. „Ich glaube, die meisten Gründer sind süchtig nach Leiden. Ja, das stimmt. Süchtig nach Elend.“ Sie stellt dies als notwendig dar, nicht als edel: „Normalerweise sind diese Gespräche das, was man am Ende wählt – ausgewählte Investoren. Sie haben einige sehr aufregende Gespräche. Aber aus dieser großen Anzahl eher langweiliger Prozesse gab es einige sehr aufregende Gespräche.“ Die Risikokapitalgeber, die nach Gründern mit einem „Chip auf der Schulter“ suchten – Menschen mit vergangenen Narben, die in unerbittlichen Antrieb umgewandelt wurden –, fanden in Hong jemanden, deren gesamte akademische Karriere eine Reihe wahrgenommener Misserfolge war, die in Motivation umgewandelt wurden.
Dies zeigt sich darin, wie Axiom mit Herausforderungen umgeht. Als der AxiomProver anfangs ein Putnam-Problem nicht lösen konnte, das geometrische Einsicht erforderte, zeichnete Professor Evan Chen (Trainer des US-IMO-Teams) ein Bild, und jeder im Raum sah sofort die Lösung. Die KI fand schließlich durch erschöpfende Aufzählung einen völlig anderen Beweis. „Ich denke, wenn man Menschen und KI vergleicht, ist die Mathematik hinter der Lösung, die wir erhalten haben, ein sehr interessanter Prozess“, reflektiert Hong. Der Vorfall kristallisierte eine Kernspannung heraus: Intuitive Mathematiker bieten Eleganz und Einsicht; KI bietet erschöpfende Zuverlässigkeit und Verifikation. Beides ist notwendig.
Mit Blick auf die Zukunft beschreibt Hong KI für Mathematik als Ermöglichung eines Übergangs von einer „mathearmen zu einer mathereichen Gesellschaft“. Das Angebot wird explodieren. Aber sie weist die Darstellung zurück, dass dies die Mathematik weniger besonders mache: „Ich denke, für unsere Mathematiker liegt die Bedeutung zu einem großen Teil darin, Probleme zu lösen. Sie werden 0,01 % Intuition darüber liefern, welche Matheprobleme es wert sind, dass wir unsere Rechenleistung darauf konzentrieren, sie zu lösen.“ In einer Welt mit unendlicher Rechenleistung wird diese Rolle der Ressourcenallokation weniger kritisch – „wir werden das tun, wir wollen alles tun, was sich Menschen ausdenken können, alle neugierigen Matheprobleme gelöst.“ Aber in der Praxis bleibt die Rechenleistung begrenzt, und das menschliche Urteilsvermögen darüber, was wichtig und was trivial ist, bleibt unersetzlich.
Die letzte philosophische Frage – was, wenn KI die Mathematik langweilig macht, indem sie alles löst – veranlasst Hong dazu, auf die menschliche Natur zurückzukommen. „Gib mir eine mit 1 Million Zeilen Lean-Code, ich muss sehen, wie es im Inneren gemacht ist. Du wirst mich nicht sehen lassen, ich werde hingehen und es sehen. Das ist die Verkörperung menschlicher Neugier.“ Sie verweist auf Beispiele wie Stefano Ermon, der Diffusionsmodelle schneller macht, oder Periodic Labs, die Top-KI-Talente für komplexe reale Probleme der Materialwissenschaft gewinnen, oder Recursive, die an Hardware-KI-Co-Optimierung arbeiten. „Dahinter steht eine grundlegende Kraft. Diese grundlegende Kraft ist die menschliche Neugier. Manche Leute sagen, es ist jetzt eine Blase, oder sollten wir sagen, es ist jetzt die Mondlandung? Manche Unternehmen, sobald er er selbst wird, wird er zum Mond fliegen. Dann gibt es Unternehmen, die zum Mond fliegen – sie arbeiten wirklich hart, jeder arbeitet wirklich 996 jeden Tag zusammen auf diesen Traum hin. Es hat nicht geklappt. Das ist die Blase.“
Axioms Wette ist, dass formale Verifikation, rekursive Selbstverbesserung und ein Systemansatz für das Denken eine verteidigbare Position in einem Markt schaffen, in dem DeepSeek Basismodelle über Nacht zur Massenware machen kann. Das Unternehmen positioniert sich „eher wie SpaceX“ als ein typisches KI-Labor – es geht technische Herausforderungen mit riesigen technischen Barrieren an, die über das Training größerer Modelle hinausgehen. Ob diese Wette gelingt, bestimmt nicht nur das Schicksal des Unternehmens, sondern möglicherweise auch den Zeitplan dafür, wann Maschinen sinnvoll zur Grenze des mathematischen Wissens der Menschheit beitragen können. Hong scheint mit der binären Natur dieses Ergebnisses zufrieden zu sein, vielleicht weil ihre gesamte Laufbahn eine Reihe unwahrscheinlicher Erfolge war, die wie Misserfolge auf dem Weg dorthin aussahen. Wie sie es ausdrückt: „Es gibt immer einen Weg. Man muss daran glauben.“