Fünf von KI generierte mathematische Artikel wurden angenommen, und der Gründer aus der Generation nach 2000, Hong Letong, hat 1,4 Milliarden Yuan an Kapital beschafft.

In den Preprints von mathematischen Artikeln haben sich heimlich 8 AI-generierte Werke eingeschlichen.

Genauer gesagt sind es 8 mathematische Artikel, die von demselben System generiert oder formal bewiesen wurden.

Das Startup Axiom Math hat angekündigt, dass von den 8 Artikeln, die sie seit Februar 2026 eingereicht haben, bis zum 28. Mai 5 bereits die Peer-Review bestanden und in Fachzeitschriften veröffentlicht wurden.

Die Gründerin Hong Letong wurde 2001 in Guangzhou geboren. Sie absolvierte in drei Jahren an der MIT ein Doppeldiplom in Mathematik und Physik und gewann die höchsten Auszeichnungen für nordamerikanische Mathematikstudenten, den Rhodes-Stipendium und den Morgan-Preis.

Während ihres Promotionsstudiums an der Stanford-Universität hat sie sich zurückgezogen.

Der Grund für ihren Rückzug war die Gründung von Axiom Math.

Axiom hat im März eine Finanzierung von 2 Milliarden US-Dollar (etwa 1,356 Milliarden Yuan) abgeschlossen und hat einen Schätzwert von 1,6 Milliarden US-Dollar (etwa 10,846 Milliarden Yuan).

Die eingereichten Artikel erstrecken sich über die Zahlentheorie, die Kombinatorik, die kommutative Algebra, die algebraische Geometrie/geometrische Dynamiksysteme, die Darstellungstheorie und das Dyck-Pfad-Modell.

AI-Bewertung, maschinelle Prüfung, menschliche Begutachtung

Um zu verstehen, was Axiom Math macht, sind diese 8 Artikel der beste Ausgangspunkt.

Einer der Artikel, "Reciprocals of Partition Polynomials", wurde von den "Annals of Acad. Rom. Sci." akzeptiert.

Dieser Artikel untersucht die Konstruktion von reziproken Summen aus partition subsum Polynomen. Ziel ist es, 10 Vermutungen von Ballantine, Beck, Feigon und Maurischat zu behandeln.

Die AI hat 6 von ihnen bewiesen und ein Gegenbeispiel in der ursprünglichen Aussage gefunden.

Dieses AI-System heißt AxiomProver und erzeugt Artikel, die nicht nur in natürlicher Sprache vorliegen, sondern auch formale Beweise enthalten.

Große Modelle können Texte schreiben, die wie Beweise aussehen.

Das Problem ist jedoch, dass selbst die glattesten Beweise in natürlicher Sprache logische Lücken enthalten können. Leser, Gutachter und Autoren müssen sich auf ihr Verständnis verlassen, um zu entscheiden, was stimmt.

AxiomProver bietet eine andere Art der Abgabe:

Forscher geben eine Problemstellung in natürlicher Sprache an, und das System übersetzt das Problem in einen formalen Beweis in Lean. Anschließend wird jeder Schritt von einem separaten Detektor überprüft.

Der Text der Artikel wird von menschlichen Mathematikern mit einer akademischen Erklärung versehen.

In diesem Experiment hat die AI nicht die Menschen ersetzt, sondern ein neues Modell der Mensch-Maschine-Kollaboration praktiziert.

Die AI ist für die Generierung oder formale Prüfung von Beweisen verantwortlich, während menschliche Mathematiker für die Problemformulierung, die Erklärung der Artikel und die Kommunikation mit den Gutachtern zuständig sind.

Der Gründermathematiker von Axiom, Ken Ono, hat angegeben, dass das System in einigen Fällen binnen etwa 24 Stunden einen vollständigen, maschinell verifizierten Beweis für ein offenes Forschungsproblem generieren kann.

Von einem Post-00 chinesischen Gründer gegründet, mit Fokus auf verifizierbarer AI

Die Gründerin Hong Letong hat schon in jungen Jahren außergewöhnliche mathematische Begabung gezeigt und sich mit der Unterstützung ihrer Eltern in Mathematikwettbewerben engagiert.

Mit 14 Jahren hat sie "MIT" auf einem Zettelt geschrieben, um sich selbst zu motivieren.

Während ihrer Zeit in der High School besuchte sie die Affiliierte Schule der Südchina Normal University, wechselte in die Provinzmannschaft für das chinesische Mathematik-Olympiade und gewann mehrere nationale Mathematikwettbewerbe.

2019, im Alter von 17 Jahren, wurde Hong Letong an die MIT aufgenommen und absolvierte in nur drei Jahren ein Doppeldiplom in Mathematik und Physik. Während ihres Bachelorstudiums hat sie 9 wissenschaftliche Artikel veröffentlicht.

Nach ihrem Bachelorstudium absolvierte sie einen Master in Neurowissenschaften an der Universität Oxford und kam erneut in Kontakt mit künstlicher Intelligenz und maschinellem Lernen.

Anschließend wurde sie für ein Doppeldiplom in Mathematik und Rechtswissenschaften an der Stanford-Universität akzeptiert.

Um sich ganz der Unternehmensgründung zu widmen, hat sie im Herbst 2024 von der Stanford-Universität abgebrochen.

Ihr Geschäftspartner Shubho Sengupta hat ebenfalls von Meta gekündigt. Beide haben sich von den Kreuzungsmöglichkeiten zwischen AI und mathematischer Logik inspirieren lassen und beschlossen, das Problem der Halluzinationen von AI zu lösen.

Später hat der bekannte Mathematiker Ken Ono seinen Lebenszeitvertrag an der Universität Virginia aufgegeben und sich vollzeit bei Axiom engagiert.

AxiomProver hat bei der Putnam-Mathematikwettbewerbung die volle Punktzahl erreicht und zwei Erdős-Vermutungen gelöst, die die Wissenschaftsgemeinschaft seit Jahrzehnten beschäftigen.

Aber der "AI-Mathematiker" ist nur der erste Schritt von Axiom Math. Ihre Vision ist es, einen sich selbst verbessernden Superintelligenz-Inferenzrechner zu schaffen.

In weniger als einem Jahr hat Axiom eine 64-Millionen-US-Dollar-Saatfinanzierung und eine 2-Milliarden-US-Dollar-Reihe-A-Finanzierung abgeschlossen, und der Schätzwert ist auf 1,6 Milliarden US-Dollar gestiegen.

Der Investor Matt Kraning hat das Unternehmen so bewertet: "Die AI wird all den Code schreiben, aber die Mathematik wird beweisen, ob er funktioniert."

Wenn ein AI-System mathematische Beweise maschinell Schritt für Schritt überprüfen kann, könnte dieselbe "Generierung, Formalisierung, Verifizierung"-Schleife auch für andere Disziplinen und risikoreiche Entscheidungsfindungsszenarien verwendet werden.

Am 27. Mai hat Axiom einen neuen Artikel eingereicht, der in die Gebiete der Spieltheorie und Ökonomie vorstößt.

In Zusammenarbeit mit dem Harvard Business School-Professor Scott Duke Kominers wurde ein klassischer Satz von Robert Aumann mit Lean formal bewiesen.

Hong Letong hat einmal gesagt, dass Unternehmer die schwierigsten Probleme wählen sollten, die vielleicht 5 bis 10 Jahre dauern, um gelöst zu werden.

Es scheint, dass der Weg, den sie gewählt hat, auch einer der am meisten beobachteten ist.

Referenzlinks:

[1]https://x.com/axiommathai/status/2059640254341284320

[2]https://axiommath.ai/papers

Dieser Artikel stammt aus dem WeChat-Account "QbitAI", Autor: Meng Chen. 36Kr hat die Veröffentlichung mit Genehmigung durchgeführt.