The Beauty of Mathematics, Part 3: The Moonshot
She doodled MIT on her math scratch paper in Guangzhou. A decade later, she raised $1.6 billion to teach machines to prove.
This 3-part deep-dive series explores a four-hour interview with Carina Hong, hosted by Xiaojun Zhang in 2026. To better convey the depth and ideas of the conversation, I have reorganized the narrative, added background context, and clarified some of the more technical points.
Carina Hong describes her own company in terms that most founders have scrubbed from their talking points before the pitch meeting begins. “The outcome is binary,” she says. “Either we land the moon, or we do not. There is no middle.” She says this in multiple registers across the interview, sometimes analytically, sometimes with a slight shrug, and always with the calm of someone who has done the math on what happens if the rocket fails. She was twenty-four when she founded Axiom Math in July 2025. She turned twenty-five while raising $200 million at a $1.6 billion post-money valuation in March 2026, led by Menlo Ventures. The business model, which she told her seed-round investors she did not yet understand, remains an open question. What is not open is her willingness to say so aloud.
The first two parts of this series unpacked what Axiom is building and why. This part turns to the person building it. Not because biography validates thesis, but because the path she took to reach this bet is unusual enough to be worth tracing, and because the specific way she tells the story, candid about the fear and the uncertainty and the days she feels the stupidest in the room, is rare in Silicon Valley. The version of the AI-founder archetype that dominates the discourse is confident, messianic, and careful. Hong is intense, honest about herself, and not careful at all.
The Doodle
Hong grew up in Guangzhou. Her walk to primary school was ten minutes, long enough to get lost in thought, which she often did. She attended South China Normal University’s affiliated high school, a feeder for Chinese academic olympiads. She competed in math olympiads. She was, by her own account, consistently unable to solve the first problem on each round, the Euclidean geometry question that the other strong students regarded as automatic. She compensated, as described in Part 2, by grinding through with complex-number coordinates. It took her two to three times as long as her classmates and produced solutions that were correct but inelegant. She lost time. She sometimes skipped later problems. She kept doing this for years.
Somewhere in this period, she started doodling “MIT” on her mathematics scratch paper. The letters, she explains with characteristic flatness, were easy to draw. “If I had wanted to go to another school, say Columbia, it would have been more letters to write. MIT is three.” She had seen Good Will Hunting. She knew MIT was where the Infinite Corridor was. She knew it was where great mathematicians and physicists and astronauts came from. The doodle became a small ritual.
There is a framework, introduced to her later by a mentor, that Hong now uses to describe her childhood mental state. It comes from neuroscience. “Bounded attention” is the attention that is focused on a task. “Free attention” is the attention that wanders. Most children, most of the time, alternate between the two. Hong’s walk to school, the daydream in class, the complex-number method itself, she now describes as free attention applied to whatever was in front of her. It felt like play. It produced persistence as a byproduct.
She got into MIT. She majored in mathematics and physics. She did not, she notes repeatedly, feel like the smartest person in any room she entered there. MIT is a school where ordinary mathematical talent looks blunted next to the kind of student who is completing Knots and Surfaces in freshman year. Hong reports, without obvious bitterness, that she felt in every phase of her life that she was the stupidest person in that environment, the one who tried hardest and saw the least.
“I kept trying things that did not work,” she says. “And I kept trying them.”
The Cure
MIT changed her not through its curriculum but through its atmosphere. “What is hard, do that,” she says, summarizing what she took from the place. “What is painful, do that. What requires long-term thinking, do that.” She describes the school’s culture of suffering with something like affection. Students running in the middle of blizzards when the red weather alert said stay inside. A peer group, she says, “every one of whom could endure.”
Then the pandemic hit. Hong had been a freshman. In her second semester, MIT sent everyone home. Her small team of friends and study partners, which she had relied on as her emotional infrastructure, dissolved into Zoom rectangles. She was alone in an apartment, taking the same hard classes, but without the group that had absorbed the pain alongside her.
She had to find something else. What she found, or so she tells the story now, was the ability to extract meaning from difficulty itself, without a peer group to share it with. “The learning curve was very steep,” she says. “MIT really shaped my character.” The phrasing is restrained. What the phrasing covers is a transition she emphasizes carefully in the interview: from someone who could tolerate suffering within a community to someone who could find something useful in suffering alone. The second is the traitful pattern that investors later told her they look for. “Founders with a chip on the shoulder,” one of them said to her. “Chips on the shoulder convert into chips in the pocket.” She heard this phrase for the first time as a VC cliché and has since stopped finding it cliché.
She now says, with some amusement and no denial, that she is addicted to pain. “A lot of founders I know are,” she says. “It is not necessarily healthy.”
The Detour
She graduated from MIT with the double degree and, for reasons that in retrospect look like test runs, followed a path through the kind of elite credentialing that mathematicians sometimes take before settling into research. A Rhodes Scholarship at Oxford, where she completed a master’s in neuroscience at Hertford College with distinctions. Research at University College London’s Sainsbury Wellcome Centre and Gatsby Computational Neuroscience Unit. A Knight-Hennessy Scholarship at Stanford to pursue a combined J.D./Ph.D. in mathematics. Along the way, the Morgan Prize, the Schafer Prize, and nine peer-reviewed publications by the age of twenty-four.
She also spent a period as a quantitative trader. Not long, but long enough to form a view about what she did not want to do. The view is specific. In quantitative finance, she notes, your signal arrives quickly. You are right or wrong within a trading day, a week, a month. The feedback loop is so tight that it eats your own epistemic judgment. “You lose the ability to think about long-term things,” she says. “Competition in a short time horizon creates mediocrity.” The phrasing is more compressed in her voice than it looks on the page. The lesson she took from the quant period, the lesson she says she thinks about now, is that she wanted to work on problems where the signal was slow enough to let her think.
She was in her first year at Stanford, enrolled in both the law school and the mathematics Ph.D. program, when she decided to stop.
The Conversation
The founding story, like most founding stories, is cleaner in retrospect than it was in the moment. The short version, the one that appears in secondary coverage, is that Hong met Shubho Sengupta over coffee in Palo Alto, talked for a few hours about whether AI could be a mathematician, and started a company. The version Hong tells in the interview is longer by about a year and a half.
Sengupta, who became Axiom’s chief technology officer, is a generation older than Hong. He led Meta FAIR teams that developed OpenGo and CrypTen. Before Meta, he worked on distributed training systems that shaped Google Brain and was among the earliest CUDA developers at Nvidia. He has the kind of resume that, in Silicon Valley, opens doors without a further explanation of who the person is. None of this was known to Hong when she met him. They met at Verve, a coffee shop in downtown Palo Alto, where Hong was a law-school regular lugging three-volume constitutional-law casebooks and ordering matcha to watch the dogs in the courtyard. Sengupta was also a regular. They ended up at the same six-person communal table. The first conversation, as Hong remembers it, began when she asked him to close a blind because the sun was in her eyes.
They were friends for a year and a half before either of them mentioned starting a company. Hong did not know Sengupta worked at Meta. Sengupta knew she was a Stanford law and math student but not that she had a research background. They talked about the history of science, the papers Terence Tao was writing on formal proof, the Lean community, the question of whether formal verification was finally ready for AI. “We did not talk about a company,” Hong says. “We talked about the hypothesis. Could we build an AI mathematician.”
The decision itself came in the fall of 2024. Hong had just started her math Ph.D. at Stanford and was spending the other half of her time working at XTX, a quantitative finance firm with the kind of compute budget that made her realize how fast AI-for-math could move outside a university. One morning, after a run, she walked into Verve, sat down with Sengupta, and said: if we wanted to raise money for this, how much would we need. They worked out the answer on a napkin. By November she had decided. The formal fundraising would wait until Christmas, because the Christmas break was when Sengupta had time to read.
That reading group is the scene Hong mentions with the most enthusiasm. The two of them, over the break, went through what Hong calls “the Christmas reading package,” a set of papers they had assembled themselves. One of them was a survey co-authored by Kaiyu Yang and Gabriel Poesia, titled “Formal Mathematical Reasoning: A New Frontier in AI.” Hong had read across the AI-for-math literature before but had never seen the landscape laid out as a single connected surface. The survey’s fifth section proposed a set of capabilities a “good AI mathematician” ought to have, organized into a two-dimensional grid.
“I took the grid,” Hong says. “I traced every paper the survey cited, and every paper those papers cited. About half the citations I had not read. By the time I finished, the field had gone from five or six separate things I knew about to a single picture.”
The picture was the thesis. The next question was who else to bring.
The Mathematician Who Refused
Hong’s hiring strategy, for the first six months of Axiom, was an explicit rule: no mathematicians on staff until employee number fifteen.
The reasoning was not that mathematicians were useless. The reasoning was that mathematicians from the research culture would import assumptions that would slow the team down. Axiom needed to scale. It needed to train models on enormous datasets. It needed to accept that a good research proof and a good training example were not the same object. A mathematician steeped in the craftsmanship ethic of pure math, one who treats each proof as a hand-made thing worthy of years of care, would resist the industrial scaling that an AI company required.
She knows this because she tried to hire one anyway.
Early in the seed round, Hong approached a researcher connected to a benchmark in formal mathematics, someone whose technical judgment was exactly what Axiom needed. She made an offer. He accepted. Then he withdrew. The reason he gave, in Hong’s telling: “I do not want to work on internet-scale datasets.”
“He saw math as craft,” she says. “Sushi made one piece at a time. We were going to ask him to scale everything. He was right to withdraw. And I was right to try.”
The experience shaped her hiring approach. When she eventually did start bringing mathematicians in, Ken Ono first, the criterion was not credentials. It was openness to a specific kind of adversarial collaboration. Hong’s phrasing is precise. “We want mathematicians who fight us.” The mathematicians Axiom hires are not there to do the AI work. They are there to build benchmarks the AI cannot yet solve, to point out where the system’s proofs are technically valid but mathematically unsatisfying, to produce the training-signal shape that a self-play loop could not produce on its own. Adversarial. Not antagonistic, but structurally oppositional. The mathematician’s job is to find the gap. The engineering team’s job is to close it. Then a new gap is found. The cycle iterates.
Ken Ono, the fifty-seven-year-old mathematician whose arrival generated the “tenured professor quits to work for twenty-four-year-old” headline in Chinese media, joined under this arrangement. Ono, as discussed in Part 2, was hired specifically as a conjecturer. But he was also hired, Hong says explicitly, as someone who was going to push back. “His job is to tell us when we are wrong. He tells us often.”
This hiring principle extends to everyone. Sengupta fights Hong on engineering choices. The benchmark-focused mathematicians fight the prover team on evaluation criteria. François Charton, the Meta researcher who first applied transformers to mathematics in 2019 and who came to Axiom after using LLMs at Meta to solve a century-old math problem and disprove a 30-year-old conjecture, fights on how the mathematical and the machine-learning cultures should interface. The adversarial rule is a culture, not a tagline. Hong does not pretend it is comfortable. “It is exhausting,” she says. “But it works.”
The Fundraising
The fundraising story, told in pieces across the interview, is the most revealing section for anyone who has ever raised money and suspected the process had an absurd theater to it.
“Nobody likes fundraising,” Hong says. “Nobody. If I could pay an AI a percentage to raise for me, I would.” The reason, she explains, is not difficulty. The reason is repetition. “You are a repeating machine. You say the same things to one investor that you said to the last. You get the same questions. You give the same answers. After three weeks you could record yourself and send the recording instead.”
She describes an elevated signal-to-noise experience with Howard Morgan, the co-founder of Renaissance Technologies and First Round Capital, currently the chair of B Capital, the firm that led her seed round. Morgan is eighty years old. He was an early user of the ARPANET, with machine number fifty on the network in the early 1970s. He has been an active investor for more than forty years. When Hong met him, she had been awake most of the night rewriting a paper rebuttal for an academic conference deadline. The Zoom call was wedged into a gap. She went into it tired and not particularly polished.
What she did not expect was that Morgan, who by that point in his career had heard thousands of pitches from thousands of founders, turned the tables. He did not ask her what her business model was. He told her what her business model was. He laid out, with more conviction than she had at the time, where Axiom’s commercial paths were and how they would unfold. “He was more optimistic about my company than I was,” Hong says. “That does not happen often with investors.”
This is the moment she cites as the one that converted fundraising from theater back into something like genuine conversation. Her anti-pitch style, she had realized, was working because it was unusual. “Most founders tell VCs things are a ten out of ten,” she says. “The VCs apply a discount. They end up hearing an eight. I told them we were a seven. So they applied a discount and heard nothing.” She laughs. “But the ones who liked that I told them it was a seven, those were the ones I wanted anyway.”
The competitive dynamics worked in her favor once the first offers arrived. From the first term sheet to the last, the price tripled. By the end, multiple firms were competing, and the process, which she had described initially as exhausting, briefly became interesting. “You meet people you would not otherwise meet,” she says. “Occasionally one of them changes how you see your own company.”
The Landscape
One of the questions the interviewer asks, and which every founder in AI has to answer, is why large labs do not do what Axiom does. OpenAI, Google DeepMind, Anthropic all have both the talent and the infrastructure. Several of them have teams working on formal math. Why is there space for a startup?
Hong’s answer is specific and not defensive. “They could do it,” she says. “But they will not, because the expected return on that talent in their current focus areas is higher.” OpenAI’s informal-reasoning work, she notes, is driven by a senior researcher’s personal ambition for scientific discovery. Google DeepMind has parallel teams, one on formal methods and one on informal, and AlphaProof is their public flagship. Anthropic uses Lean data as a reinforcement-learning reward signal but treats it as infrastructure, not as a core product direction. The structural fact, in her framing, is that a lab with a dominant commercial product cannot redirect its best people to formal verification. The opportunity cost is too high. A startup with no other product can.
The real competitor, she says, is Harmonic, a company co-founded by the Robinhood CEO that has raised $295 million at a $1.45 billion valuation. The two companies share the broad thesis that verification matters, and differ on architecture. Harmonic, Hong notes, has a founder whose attention is split between Robinhood and the startup, which creates a different dynamic. “Their energy is scientific ambition,” she says, in a phrasing that sounds like praise and is also a differentiator. “Ours is moonshot.” The distinction, as she draws it, is that a scientifically ambitious company can afford to explore. A moonshot company has to land.
She is also clear that the labs could eventually become partners rather than competitors. “OpenAI sub-contracts search to Bing,” she offers as a parallel. “A large lab focused on informal reasoning could eventually invoke a formal prover, built by someone else, when a formal proof is required.” This pattern, she predicts, is where Axiom’s commercial opening is largest: as the verification layer for code-generating AI systems built by other companies.
The Moonshot
The word she uses for her company’s ambition, the word that organizes the interview, is moonshot. She uses it in English, embedded in Mandarin sentences, because the Chinese translations do not carry the same connotation. She invokes SpaceX, deliberately. Rockets that either reach orbit or burn. Companies that either return to earth having completed the mission or crash trying. The binary outcome is structural. There is no small win.
“I believe in recursive self-improvement,” she says. “I think it is near-term achievable, and I think verification is the piece that unlocks it. If I am wrong, we do not get a partial version of it. We get nothing. If I am right, everything changes.”
The phrasing is not standard startup talk. Most founders hedge. Most founders describe their companies as asymmetric bets, the small chance of a huge win against the likely chance of a modest one. Hong does not. She describes her company as an all-or-nothing bet, and she asks investors to join her on that basis, and she seems perfectly aware that this framing selects for a specific type of capital and deselects everyone else. It also selects for her own continued commitment, which is a function she has thought about explicitly.
“If we fail,” she says, in response to a direct question, “I might go back to neuroscience. I want to understand the brain. Current brain-computer interfaces are nowhere close to what they need to be. That is a problem I think about.”
She says this easily. Not as a fallback. As a parallel life that exists in a different branch of the probability tree, and that she would find meaningful if she had to take it. The detail matters. A founder who has already made peace with what they would do if the company failed is a specific kind of founder. Not a desperate one. Not a reckless one. Someone who has accepted the binary and chosen the moonshot anyway.
Language Is the World
Near the end of the conversation, Xiaojun Zhang mentions that her production company is called “Language Is the World” Studios. The name is a philosophical position as much as a brand: that language is the medium through which reality is structured and communicated. She asks Hong what she thought of the name when she first encountered it.
Her answer, at the end of four hours of discussion about Lean, about Curry-Howard, about verification and conjecture and the elegance filter and the question of whether beauty can be trained, is characteristic. “Mathematicians,” she says, “have been writing code in natural language for thousands of years. That is what a mathematical proof is. Structured logical reasoning, expressed in English or Chinese or whatever natural language the mathematician writes in. The thing that is new in the last decade is that we now have a second way to write proofs, in formal languages like Lean, and we can run them through a compiler. What we are doing at Axiom is building the bridge between the two ways of writing.”
The remark is offered in passing. It is also, in a sense that connects back to Part 1 of this series, exactly the thesis of the series. Math is code. Code is math. The reason this is not a metaphor is that natural-language mathematics and formal mathematics are two expressions of the same object. Hong’s company is betting that the translation from the first to the second, and the closed-loop verification that becomes possible when both exist, is the missing capability of the current AI paradigm. The word for that capability is proof. The word for the company is Axiom, which is the name for the starting point of a formal system, the smallest set of assertions from which the rest of mathematics can be derived.
She is twenty-five years old. She believes the closed loop can be built, that recursive self-improvement is near-term, and that Axiom’s binary outcome will be known within a few years. She has raised $1.6 billion worth of capital from investors who agree with her on enough of the thesis to fund the attempt. She grew up walking to a primary school in Guangzhou, doodling three letters on her scratch paper because those three letters were the shortest path from where she was to where she wanted to be.
The rocket is built. The launch window is open. Whether it lands remains to be seen.
This concludes The Beauty of Mathematics series. For earlier parts: Part 1, “Math Is Code”; Part 2, “Proofs from The Book.”