Math Prodigy Hopes to Make AI Smarter with Math-Based Model
By Tom Kagy | 07 Dec, 2025

Carina Hong started Axiom AI to build an AI mathematician that can model the real world more efficiently than human mathematicians.

A young mathematician who rhapsodizes about the "dopamine hit" she gets from solving math problems may well harbor a mind capable of pushing the limits of intelligence — human and artificial.  

While the AI industry is seeking ways to build machines to take over human tasks, Carina Hong wants to build an AI model that extends human capability rather than merely automating it.  Axiom AI is the embodiment of that synthesis — a machine that can propose the laws of nature, guided by a mind that has spent her life searching for them.

Carina Hong has absorbed more than her share of human knowledge.  She has progressed from math Olympiads growing up in Guangzhou to double MIT degrees in math and physics, to a 2022 Rhodes scholarship to Oxford for a masters in neuroscience, to the pursuit of a combination JD and Math PhD at Stanford.  

Hong never completed her Stanford degrees.  By early 2025 she was ready to launch Axiom AI to apply AI to math and math to AI to speed up formalization of the real world.  In short Axiom would build an AI mathematician, a model capable of efficiently distilling into formulas the mathematical laws hidden inside complex natural and economic phenomena to generate better mathematical models of the real world than even the most gifted human creators.

When Hong was ready to bring Axiom AI out of stealth mode, the venture world quickly understood the need she saw and backed her vision with $64 million in funding, valuing her startup at about $300 million.

An AI Mathematician

Hong had seen that in addressing hard scientific problems like drug discovery, climate modeling, fluid dynamics, AI systems could fit data, but they struggled to generate explicit mathematical expressions that described the underlying phenomena.  Neural networks could approximate a system, but they couldn't articulate it.  Hong quickly understood that these limitations would keep AI’s greatest contributions locked inside opaque numerical weight matrices but was useful but not capable of surpassing the human capacity for innovation.

She founded Axiom on the belief that scientific progress depends on the discovery of interpretable formulas, not just accurate predictions.  It focuses on building AI models that can autonomously generate symbolic mathematical expressions explaining how systems evolve. These are not simple regression equations. They are candidate physical laws, compact analytic expressions that can reveal the deep structure of real-world systems—from how proteins fold to how financial markets propagate shocks.

Neural-Symbolic Architecture

The first breakthrough came when Hong and her small team built a neural-symbolic architecture capable of searching an immense space of possible functional forms. Traditional symbolic regression approaches, such as genetic programming, tend to collapse under the combinatorial explosion of formula trees. Axiom’s key insight was to combine machine-learning-driven pattern recognition with a constrained symbolic search guided by mathematical priors. The result was a system that could generate meaningful formulas in minutes rather than weeks.

Encoding an Instinct for Mathematical Taste and Aesthetic Reasoning

But the real innovation, Hong explains, is not raw computational power. It is the encoding of mathematical “taste”—a sense of what makes certain formulas elegant, generalizable, or physically plausible.  Human mathematicians have this instinct naturally, but it is rarely formalized. Axiom created a scoring system that evaluates formulas not only for predictive accuracy but also for conceptual elegance: parsimonious structure, symmetry, differentiability, invariance properties, and consistency with first principles. The system learns from vast corpora of human-written mathematics and thousands of candidate models it produces on its own, continually refining its sense of what a “good” formula should look like.

This blend of brute computational search and human-inspired aesthetic reasoning is what allows Axiom’s AI to outperform expert human mathematicians on many modeling tasks. For example, Axiom’s system has discovered formula families that match or exceed classical turbulence models in fluid mechanics—a notoriously difficult domain with open problems still unresolved by physics. It has also uncovered interpretable models for ecological population dynamics and complex supply-chain behavior that previously required massive simulations to approximate. The company’s demonstrations, some of which circulate quietly among research institutions, show the AI consistently converging on analytic expressions that capture hidden relationships with striking accuracy.

Leading from the Trenches

Hong’s leadership style resembles that of a principal investigator rather than a Silicon Valley executive. She spends much of her time studying the system’s output, refining its constraints, and challenging it with increasingly abstract or messy systems. Colleagues describe her as methodical but wildly imaginative — like a mathematician who thinks in legal-style hypotheticals and an attorney who thinks in geometric structures. This duality manifests in Axiom’s culture, where engineers work side-by-side with mathematicians, physicists, and quantitative lawyers to embed deeper reasoning into the AI’s architecture.

What makes Axiom’s approach especially compelling is the potential for real-world application. In biology, interpretable formulas can reveal functional mechanisms that black-box predictors obscure. In finance, symbolic models can expose causal structures behind market volatility. In engineering, explicit analytic expressions allow faster optimization than simulation-based systems. And in academic mathematics, the system may one day generate conjectures that push the frontier of theoretical discovery.

Industries with Pressing Modeling Problems

Axiom has attracted attention not only from scientific institutions but also from industries facing pressing modeling problems.  Climate-risk modelers have tested Axiom’s formulas to better understand the nonlinear behavior of atmospheric processes.  Pharmaceutical firms have explored its use in constructing interpretable mechanistic models of molecular interactions. Even logistics companies have experimented with its AI to uncover hidden patterns in network delays and route congestion. In each case, the appeal is the same: formulas that both predict and explain.

For Hong, the mission goes beyond commercial opportunity. She sees Axiom as part of a broader reevaluation of what scientific intelligence means. If machines can autonomously produce new mathematical knowledge, then humanity’s role shifts from being sole creators of formal reasoning to being curators, interpreters, and collaborators with non-human minds. This does not diminish human intellect; it expands the canvas on which it operates.

Her vision of the future of mathematics is more collaborative than competitive. She imagines teams of humans and AI working together—machines generating candidate laws and humans providing conceptual grounding, intuition, and rigorous proof. In this world, mathematical discovery accelerates dramatically, opening new territories in physics, biology, economics, and beyond.

Axiom remains a young company, but Hong’s ambitions are nothing short of transformative. She wants to build systems that reveal the hidden equations behind everything from protein dynamics to macroeconomic cycles. She wants to democratize access to high-level scientific modeling. And ultimately, she wants to give humanity tools to see the world through entirely new mathematical lenses.

Guangzhou to Stanford

Carina Hong was born about 24 years ago in Guangzhou, China.    By middle school she was competing at levels usually reserved for exceptional high-schoolers.  By high school she could already boast accomplishments that would guarantee her a place at the top ranks of competitive mathematics in the United States.  She represented China in elite problem-solving competitions and built a reputation for unusual pattern recognition: an ability to see the “shape” of a solution before she could fully articulate it. Teachers described her as unusually attuned to the structures behind equations, as if she could sense mathematical relationships spatially rather than merely symbolically.

Her local Math Olympiad exposure provided her with the thrill of solving "super fun problems", instilling in her a deep love for the rigor and intellectual travel that mathematics offers.  She quickly distinguished herself, thriving in the competitive environment where she was one of only a handful of women to make it to the final stages of the provincial team. This foundation in competitive problem-solving was the crucible that forged her unique approach to grand challenges.

She achieved her early ambition to attend MIT and became a legend in her three years there.  While completing dual undergraduate degrees in Mathematics (Course 18) and Physics (Course 8), a rare feat, but she also took over twenty graduate and doctoral-level courses while publishing nine peer-reviewed papers spanning number theory, combinatorics, theoretical computer science, and probability. This brilliant undergraduate record led to her winning the two highest honors for an undergraduate mathematician in North America: the AWM Alice T. Schafer Prize(awarded to one undergraduate woman annually) and the AMS-MAA-SIAM Frank and Brennie Morgan Prize for Outstanding Research.

In 2022 she won a Rhodes Scholarship, one of only four Chinese recipients that year.  While at the University of Oxford she earned an MS in Neuroscience, conducting deep learning research at University College London’s Gatsby Unit. This pivot to biomedicine was driven by a desire to "understand biology more," seeking a mental model that spanned the scientific space from the abstract logic of math to the messy complexity of life.

She continued challenging herself by pursing a a joint program for a PhD in Mathematics and a JD in Law, supported by the Knight-Hennessy Scholarship.  This move into law was particularly striking, showing a dedication not just to solving technical problems, but also to understanding their societal, ethical, and structural implications.  She found intellectual stimulation in contracts and antitrust and constitutional law, but couldn't resist the call of deep technical problem-solving.

She dropped out of her Stanford joint JD/PhD program at Stanford to dedicate herself to the vision of building a self-improving superintelligent reasoner, starting with an AI mathematician.  The funding Axiom showed faith in Hong's core thesis: that the current generation of large language models (LLMs) is fundamentally limited by its reliance on statistical prediction, often leading to hallucinations and a lack of verifiable truth.  Axiom aims to fix this by building an AI whose output is not probable but provable.

The technical approach hinges on leveraging formal proof languages like Lean. These languages allow mathematical statements and their proofs to be encoded in a machine-verifiable format. Axiom’s work focuses on solving the massive data gap between general-purpose code and formal mathematical code, and on the challenge of autoformalization — the automatic translation of human, natural - language proofs into the machine-verifiable formal language.  Axiom is building a self-improving system using a self-play loop of conjecturing and proving, enabling the AI to autonomously discover new mathematical knowledge and continuously refine its own reasoning capabilities.

Naturally, the claim that AI might surpass human mathematicians is controversial. Many researchers argue that creativity in mathematics is fundamentally human, tied to intuition and conceptual leaps no machine can replicate.  Hong agrees that human creativity is indispensable — but she draws a distinction between artistic invention and structural discovery.  Human mathematicians are brilliant, she explains, but also limited by cognitive bandwidth and heuristic biases.  AI, unconstrained by these limitations, can traverse landscapes of mathematical possibility too vast for any individual. Humans will still interpret, generalize, and refine these discoveries. But machines, she believes, will increasingly generate them.