This is the overture to The Beauty of Mathematics, a series built from a four-hour interview with Carina Hong, hosted by Xiaojun Zhang, about her bet that machine-checkable proof, not generation, is the foundation of superintelligence.
In December 2025, an AI system sat the Putnam, the hardest undergraduate math competition in the world, and scored a perfect twelve out of twelve. In the exam’s ninety-eight-year history, only five humans had ever done that. One of those five, Evan Chen, had solved one of the problems with a single diagram. The AI, a system called AxiomProver, solved the same problem too, in a formal proof running four thousand lines long. Both proofs were correct. Neither the diagram’s economy nor the machine’s length is the point. The point is that both were checked, not guessed, and a proof-checker cannot be talked into accepting a wrong answer with a confident enough tone.
Carina Hong is twenty-four years old. She studied math and physics at MIT, held a Rhodes Scholarship at Oxford, then dropped out of a joint PhD and law degree at Stanford to found Axiom Math. Investors have since put $1.6 billion behind her, including a $200 million round led by Menlo Ventures, on a claim that runs against the grain of everything the rest of the AI industry is building. The industry’s paradigm is generation: predict the next token, the next pixel, the next action, and hope the result is right more often than it is wrong. Hong’s claim is that generation without verification is confidence without a foundation, and that formal mathematics offers something almost nothing else does, a domain where a claim’s correctness can be checked by a machine, absolutely, with no vote and no benefit of the doubt.
The technical version of the claim has a name mathematicians and computer scientists have known for decades: a theorem is a program, and a proof is that program compiling. Lean, the formal language Axiom builds on, does not grade a proof for plausibility. It runs it. What follows takes that claim seriously, at the scale Hong is betting on it, from a single exam score to a wager that verification, extended past mathematics into code and eventually into anything that can be formally specified, is not a safety feature bolted onto intelligence. It is intelligence’s foundation.
The Three Parts
Three parts, all on The Beauty of Mathematics‘s shelf.
Part 1: Math Is Code: why the same Putnam problem having a one-diagram human proof and a four-thousand-line machine proof is exactly the fault line the whole bet sits on.
Part 2: Proofs from The Book: why Erdős’s fantasy of a book holding only the most beautiful proofs turns out to be a real design question for anyone trying to teach a machine to do research mathematics, not just pass its exams.
Part 3: The Moonshot: the headline that made her famous, a tenured fifty-seven-year-old quitting his chair to work for a twenty-four-year-old, and the part of that headline everyone got wrong.
If This Is You
If you have started to suspect that an industry built on confident generation has a hallucination problem it cannot fully engineer around, Part 1 is where that suspicion meets a working alternative. Axiom’s bet is not a safety argument bolted on after the fact. It is a claim about where intelligence comes from.
Maybe you already know what Lean is, or what the Curry-Howard correspondence means, in which case the pull here is less persuasion and more a fresh account of what a proof-checking system can and cannot yet do on its own. Part 1 walks through Axiom’s Draft-Sketch-Prove pipeline and the orchestrator-and-subagents system behind AxiomProver’s score, and readers of Language Is Poison will recognize the same fight in a different costume, brute force against elegance, generation against representation, argued this time on a chessboard where every move is either legal or it isn’t.
If what draws you in is whether a machine can do mathematics rather than merely check it, Part 2 is the harder and more honest question. Hong calls herself a brute-force player, not a genius, and the gap between solving problems that are handed to you and knowing which problems are worth solving in the first place is exactly where Erdős’s Book comes back into the story.
If you are here for the business case, Part 3 is where the $1.6 billion gets a face. A twenty-five-year-old told her investors she did not know her own business model. They funded her anyway, on a bet she describes as binary: extremely good or extremely bad, with no comfortable middle where a company like this manages to survive.
And if you are not sure which of these is you, the throughline holds in one sentence: an industry that has spent years rewarding confident generation is now being tested by a system that will not accept a claim it cannot check, and Hong has put $1.6 billion behind the wager that checking, not generating, is where real intelligence lives.
A proof either compiles or it does not. Hong is betting that everything else worth knowing will eventually have to answer to the same standard.