The mathematics academic community has recently experienced a technological earthquake. The startup AI company Axiom Math has announced that its self-developed AI system has submitted 8 math papers since February this year, 5 of which have been formally reviewed and accepted by academic journals. This breakthrough not only demonstrates the huge potential of artificial intelligence in pure mathematical research, but also marks a substantial step forward for AI in solving complex academic conjectures.
Among the accepted papers, a study on the reciprocals of partition polynomials has attracted significant attention. This research directly addressed 10 core conjectures in the academic field, and the AI system successfully proved 6 of them, even identifying a counterexample in the original proposition. Unlike previous large models that only wrote "seemingly convincing" proofs in natural language, the team's AxiomProver system has introduced a new workflow: it can accurately translate natural language mathematical problems into Lean formal proofs, and each logical step is rigorously verified by an independent detector. This human-machine collaboration model—machine proof, machine check, human mathematicians polishing and explaining—fundamentally eliminates AI's "logical hallucinations."
The driving force behind this hard-core technological achievement is a 25-year-old Chinese woman. Hong Letong, the founder of Axiom Math, was born in Guangzhou in 2001 and showed extraordinary mathematical talent from a young age. She entered the Massachusetts Institute of Technology (MIT) at the age of 17 and earned dual degrees in mathematics and physics in just three years, publishing nine papers during her undergraduate studies. After obtaining a master's degree from the University of Oxford and being admitted to a dual PhD program in law and mathematics at Stanford University, she decided to withdraw from Stanford in the fall of 2024 to focus entirely on entrepreneurship.
Hong Letong's formidable background and the grand vision of verifiable AI have attracted a flood of top talent and capital. Former Meta AI expert Shubho Sengupta and renowned mathematician Ken Ono (Ken Ono) have joined as co-founders, with the latter even resigning from his permanent position at the University of Virginia. In less than a year, Axiom Math has completed two rounds of financing totaling $264 million (approximately 1.4 billion yuan), and the company's valuation has soared to $1.6 billion.
It is reported that AxiomProver had already scored a perfect score in the Putnam Mathematics Competition and solved two Erdős conjectures that had puzzled the academic community for decades. However, Hong Letong and her team's ambitions go far beyond being "AI mathematicians." Their latest research has already crossed over into the fields of game theory and economics. The team is working on applying this closed-loop reasoning ability—generating, formalizing, verifying—to other high-risk, high-precision decision-making scenarios, building a super intelligent reasoning system capable of self-improvement.
