When can AI be considered usable? A team valued at 300 million gave two words: "Acceptance."
The startup Axiom Math, founded by 24-year-old Carina Hong, is dedicated to developing an "AI mathematician" capable of independently verifying the correctness of logic. In 2025, the company secured $64 million in financing, and its core team consists of top talents from Meta and Google, as well as well-known mathematicians. Different from mainstream large models, its system uses the Lean programming language to ensure that every step of the reasoning process is traceable and checkable, thus solving the trust problem of the difficult-to-accept results produced by AI. Through its excellent performance in the Putnam Mathematical Competition, Axiom has proven that AI can shift from simply generating answers to providing rigorous formal proofs. This pursuit of credibility aims to elevate AI from an unstable auxiliary tool to a reliable collaborator that can be truly implemented and accepted in scientific research and industrial fields.
In 2025, almost every AI press conference was talking about "what we can do."
But what really stumps enterprises is another question: How can we prove that the results produced by AI are correct?
Many AI products perform well in demos before launch but encounter problems once they go live:
It's impossible to locate errors.
It's unclear who should be held responsible.
The results cannot be reproduced.
In the end, we can only say: We can't accept the results.
Axiom Math, an AI startup headquartered in San Francisco, has taken a different approach: Instead of pursuing what AI can do, it focuses on proving what it has done correctly.
This company, which completed its seed round of financing ($64 million, valued at $300 million, led by B Capital) in October 2025, is developing an AI mathematician that can independently provide answers and verify their correctness.
As a result, this team has attracted a group of people with deep technical backgrounds: former core researchers from Meta FAIR and Google Brain, as well as Ken Ono, a well-known mathematician and Carina Hong's tutor at MIT.
Carina Hong is 24 years old.
On December 21, 2025, when a media asked her how she recruited people, her answer was simple:
If the problem is difficult enough, people will naturally gather around.
This is not just empty talk. Her method is to find a difficult problem worth spending ten years solving and then wait for the real experts to come to her.
At 24 years old, with $64 million in financing and a valuation of $300 million.
What she's betting on is not just a product but the next passing line for AI.
Section 1 | At 24, Valued at $300 Million, She Wants AI to Learn Self-Proof
Her name is Carina Hong, and she was born in Guangzhou.
When she was a child doing Olympiad math problems, she had no idea that she would one day be in Silicon Valley talking about AI. But she remembers that every time she solved a problem, it was like a child clearing a game level, and she couldn't stop.
She was admitted to MIT from Guangzhou, won the Rhodes Scholarship to study neuroscience at Oxford, and finally went to Stanford to pursue a joint doctoral program in mathematics and law.
At MIT, she took 20 graduate-level math courses, published 9 papers, and studied how neural networks understand functions. At Oxford, she was at the UCL Gatsby Institute (the birthplace of DeepMind) and saw AI solving real problems up close for the first time: images, sequences, and control models.
She began to ask herself: If AI can play games and write code, why can't it do math?
The real turning point happened in Silicon Valley.
When she was a doctoral student at Stanford, she often went to a coffee shop to write papers. By chance, she met Shubho Sengupta, an AI scientist from the Meta FAIR team.
One is a mathematician who wants AI to understand math.
The other is an engineer who wants to find real problems worth solving with AI.
They talked for two hours without discussing projects or financing. They just explored a hypothesis: Can we create an AI mathematician?
After that conversation, she began to seriously consider this idea. Soon after, she dropped out of school.
She said: Some problems take too long to solve in school.
What she wants to do is not create a chatbot or a code assistant but an AI system that can verify theorems and even propose new conjectures.
This system is called Axiom, which means axiom, the most basic starting point of mathematical theory.
Starting from this point, a whole set of systems will be developed to allow AI to explore the boundaries of mathematics.
Section 2 | 9/12 in the Putnam Exam, but the Score Isn't the Point
When most people think of AI learning math, they may think of taking exams and giving answers.
But Carina says that's just the first step. What really matters is whether it knows if its answers are correct.
This is not only a mathematical problem but also an engineering problem. If the answers of AI cannot be verified, they cannot be used in critical scenarios.
Humans have a natural advantage when doing math problems: We can go back and check, prove if there are logical loopholes, if there are skipped steps in reasoning, and if the details are consistent.
Carina calls this checking process "acceptance."
But large models can't do this.
They generate a lot of content but have difficulty confirming if it's correct. Especially in mathematics, even a single wrong letter can invalidate the entire conclusion.
To solve this problem, we need formal languages.
Carina's team uses a mathematical programming language called Lean. All formulas, steps, and proofs must be written clearly like a program and can be verified by machines.
This means that it's not just about what AI says is correct; every step it takes must leave a checkable trace and finally pass the verification like software testing.
To prove that this method works, they conducted a test.
In December 2025, after the US Putnam Mathematical Competition, the toughest undergraduate math competition in the US with about 4,000 participants, Carina's team posted the results on X: AxiomProver independently solved 9 of the problems, provided formal proofs in the Lean language, and all of them passed the verification.
This is not just about getting 9 questions right; it's about AI solving the problems, checking itself, and confirming the results.
Carina says:
"We're not looking for an AI that can copy answers but a collaborator that can complete all the mathematical details."
What does acceptance really mean?
It means that AI not only has to give answers but also prove that the answers are correct.
In scenarios with low tolerance for errors, such as chip design, scientific research, and financial systems, vague answers are worthless. AI has to provide the process, explain the thinking, and accept checks.
Only when it can be accepted does it mean it can be trusted.
Section 3 | Why Are People from Meta and Google Leaving to Join Here?
What kind of team is needed to achieve this?
This team is not large, currently only having 17 people, but every person who joins is a top researcher in their field.
CTO Shubho Sengupta was accidentally met by Carina in a coffee shop near Stanford. He was originally from Meta FAIR, led the development of OpenGo and CrypTen, and was also involved in the early CUDA GPU architecture. He knows the problems with large models and why the math field is difficult.
But in large companies, the goals are too scattered. He wants to find a place to focus on solving an extreme problem.
Another core member, François Charton, has been researching how to use Transformer to solve integral problems since 2019. He doesn't overlook any details and focuses on whether the large model makes a wrong step rather than how much it can write.
There's also Hugh Leather, who combines deep learning and compilers. He's not a mathematician in the traditional sense, but he has rich experience in expressing complex logic with code.
They all left places like Meta and Google, giving up more stable research paths.
What Carina offers is not just a position but a vision: to use AI to produce verifiable mathematical results, with every step clear and every conclusion standing firm.
And this vision has attracted not only AI researchers from the industry.
In early December 2025, 57-year-old mathematician Ken Ono also resigned from his tenured position at the University of Virginia and joined Axiom full-time.
He was Carina's tutor, led multiple Mathematical Olympiad research projects, is an expert in Ramanujan theory, and has even appeared in a Super Bowl ad. He's someone who has brought number theory into popular culture.
He said that as a pure mathematician, he rarely has the opportunity to participate in things that can change the world. This time, he didn't want to miss it. He moved his family to Silicon Valley and became the 15th member of Axiom, with the title of founding mathematician.
His task is not to write code but to design difficult problems to test the limits of the model's reasoning.
Carina says that these people are willing to come not to follow the trend but to do something truly worthwhile.
"We're not just creating a product; we're defining a new standard: every formula is checkable, and every reasoning process is traceable. AI doesn't just generate an answer but shows the complete thinking process."
This is what their 17-person team is currently doing.
Section 4 | It's Not About Solving Problems but Teaching AI to Ask Questions
Defining a new standard is just Carina's first step.
What she really wants to do is to let AI learn to discover problems on its own.
They're currently researching a well-known unsolved problem in the mathematical world: the Collatz Conjecture. This problem is as simple as a primary school student's game but has puzzled researchers for decades.
The researchers at Axiom used a Transformer model to study this problem. The model didn't directly provide a proof but demonstrated another ability:
When predicting the Collatz sequence, it achieved an accuracy rate of 99.8% for trillion-level numbers.
More importantly, it can clearly explain why and where it made mistakes. There are clear patterns behind these mistakes, not random hallucinations.
What does this mean?
It means that AI is not just memorizing answers but learning mathematical thinking.
In Carina's view, they're not training AI to find known answers but to think and explore like a real mathematician.
The exploration she mentioned mainly consists of three stages:
First, express theorems in formal languages and imitate existing logical structures.
Second, verify different solutions to old problems and propose new proof routes.
Third, propose new conjectures, create never-before-seen problems, and provide mathematical justifications.
The whole process is not a random conversation like ChatGPT but a rule-based exploration in the proof space, constantly trying until a new path is found.
Why is this exploration important?
Because mathematics is the most rigorous language of humans and the underlying logic of the real world. Every mathematical breakthrough may bring leaps in these fields.
Carina believes that mathematical research used to progress at a rate of one advancement per decade, but now AI can shorten this cycle to a few months.
What an AI mathematician can do in the future is not just solve problems but redefine the problems themselves together with humans.
This is not just a matter in the field of mathematics. Whether it's cryptography, chip structure, or physical modeling, they all rely on mathematical principles that can be precisely described and tested. Once AI can achieve verifiability, it can transform from an auxiliary tool that "can only be tried" into a collaborator that "can be used with confidence."
This is exactly what Carina is betting on:
The next passing line for AI is not ability but credibility.
Conclusion | Only AI That Can Be Accepted Deserves the Name
Carina's idea is simple.
She only provides one judgment criterion: Whether what AI says is correct doesn't depend on whether people believe it but on whether it can explain itself clearly.
What Axiom Math is doing is to make AI explain clearly. It's not about making the model more human-like but making it trustworthy.
Truly useful AI doesn't rely on demos but on acceptance.
Once this standard is established, AI's entry into scientific research, finance, chips, and law will truly begin.
And she has just pushed this door open a little bit.
Original Article Links:
https://www.youtube.com/watch?v=b_UMhn8E8lI&t=264s
https://e.vnexpress.net/news/tech/personalities/building-math-ai-startup-how-24-year-old-stanford-dropout-carina-hong-is-attracting-big-tech-talent-4993367.html
https://www.businessinsider.com/axiom-math-stanford-dropout-meta-ai-researchers-startup-2025-12
https://www.turingpost.com/p/carina
Source: Official Media/Online News
This article is from the WeChat official account "AI Deep Researcher," written by AI Deep Researcher, edited by Shen Si, and published by 36Kr with authorization.