Zhang Xiaojun | 张小珺Jùn｜商业访谈录 Summary

Participants: Zhang Xiaojun (host), Hong Letong (guest, founder/CEO of Axium)

1. Key Themes

AI for Math Is a Deep Tech Engineering Problem, Not Just a Research Project

Hong Letong's core insight during her pre-founding period was realizing that AI for Math had crossed a threshold: it was no longer purely a scientific research problem but an engineering problem. This realization is what made her feel it was responsible to raise capital.

"I found that it's not necessarily a research problem — it's an engineering problem. The technology risk is not as high as it initially appeared." 01:19:16

The company Axium built 12-13 custom tools to make Lean (the formal language) run properly, including a proof verifier that is 100x faster than the community standard. This toolchain is itself a moat.

"The existing verify proof tool (comparator) was 100 times slower than ours. We had to build our own fast version, otherwise we couldn't run anything." 02:04:56

Formal Verification Is the First Real Market, Not Math Competitions

While Axium's public-facing story centers on solving Putnam and IMO problems, the real commercial opportunity is in formal verification of software and hardware — catching bugs in chips, distributed systems, and code. The chip industry, in particular, spends enormous resources on verification using outdated SMT-based tools.

"Amazon has one of the world's best automated reasoning teams. Without AI, they spent three to five years writing 260,000 lines of theorem-proving code to verify the memory isolation component of their hypervisor. AI has not improved the lives of those engineers." 03:01:40

"Verification is our best first market." 03:03:05

The Company DNA Is Multidisciplinary — Three Tribes Working Together

Axium's founding insight is that AI for Math requires three types of people working in combination: (1) pure mathematicians and competition specialists, (2) AI/RL/agents engineers, and (3) compiler/code generation engineers. No competitor has assembled all three.

"We have a lot of AI people — reinforcement learning, agents, applied AI. We have a lot of people doing code generation and compiler work... And we have mathematicians. These three groups combined produce a lot of ideas." 03:21:19

The LM Compiler team (Yang LeCun's 32B code world model contributors) is embedded in Axium alongside former IMO coaches, Lean library builders, and RL researchers.

2. Contrarian Perspectives

Mathematicians May Actually Be Negative Hires Early On (Then Became Essential)

Hong originally planned to hire no mathematicians until employee #15, arguing that deep math intuition could be an obstacle to scaling — similar to how Baidu's DeepSpeech team famously refused to hire linguists.

"We set a rule: don't hire a mathematician before the 15th employee... The Baidu team, when doing Deep Speech and Deep Voice, had a philosophy: 'We absolutely will not hire a linguist.' Similarly, some mathematicians were resistant to scaling. One candidate accepted our offer and then withdrew, saying they didn't want to work on 'internet-scale datasets.'" 01:28:17 and 01:29:18

However, once the prover was strong enough, mathematicians became the most important hires — not to prove theorems, but to generate the right problems (conjectures), since conjecture generation currently far lags behind theorem proving.

The Real AGI Path Goes Through Specialized Superintelligence, Not General AI

Hong argues that the path to powerful AI is to go deep into one narrow domain (math + code) until you can solve superhuman problems within it, then let the "fan" spread naturally — rather than trying to be general from day one.

"We're not aiming for AGI. We're aiming for ASI — Specialized Superintelligence. We're going straight for 'prove the Riemann Hypothesis' on the edge of the plate, and we'll develop a sector-shaped coverage from there. We will never cover 'winning the Nobel Prize for Literature,' but our sector will be large enough for B2B markets." 03:15:36

Conjecture (Not Proof) Is the True Hard Problem in AI for Math

Most AI for Math attention focuses on proving theorems. Hong argues the much harder and more neglected problem is generating good conjectures. A prover without a conjecturer is like a hammer with no nail.

"The conjecture generator is very hard. Unlike the proof model — where you either proved it (1) or didn't (0) — for conjectures, I have no reward signal. How do I know if my conjecture is good or bad?" 02:43:35

"We believe our competitor thinks IMO gold medals are the endgame and is pivoting to commercialization. We actually want to build the conjecture system." 03:26:47

Auto-Formalization Is Harder Than Theorem Proving and More Important

The community celebrates AI systems that prove theorems, but Hong argues the harder and more underappreciated problem is auto-formalization — converting natural-language mathematics into Lean code.

"Auto-formalization is actually harder than proving. If I want to convert a 20-page arxiv paper into Lean code, I need to decompose it into a 200–500 page blueprint. That decomposition requires extremely strong hierarchical reasoning — it's not translation, it's structural transformation." 02:46:55

"You get fewer likes on Twitter for formalizing existing math than for proving Putnam problems. But the technology is at least as hard, and I actually think it's harder." 02:46:27

3. Companies Identified

Axium

Description: AI for Math startup founded by Hong Letong (24, Guangzhou-born MIT/Oxford/Stanford alum), with co-founder Shubo (ex-Meta FAIR Director, 20 years GPU experience). ~30 employees, $64M seed at $300M valuation, A-round at $1.6B valuation led by Menlo Ventures.
Why mentioned: Built first AI system to achieve a perfect score on the Putnam Mathematical Competition (historically only 5 humans have done this in 98 years). Also achieved 98.93% on the Verina code verification benchmark vs. DeepCruver's 11%.
Quote: "In December 2025, Axium Prover achieved a perfect score on the Putnam. That's the 6th perfect score in 98 years — the first by an AI." 02:12:16

B Capital / Renaissance Technologies

Description: B Capital is a growth-stage VC; Renaissance Technologies is the legendary quant fund co-founded by Jim Simons.
Why mentioned: Howard Morgan, co-founder of both Renaissance and First Round Capital, led Axium's seed round and was described as being more bullish on Axium's commercial potential than Hong herself.
Quote: "Howard Morgan was just more optimistic about our business model than I was. He was telling me what my business model was... He's a mathematician, still teaches at NYU sometimes." 01:41:31

Menlo Ventures

Description: Tier-1 VC firm, largest institutional investor in Anthropic. Led Axium's A-round.
Why mentioned: Partner Matt Cranin (electrical engineering PhD, physics undergrad) was described as deeply technical and founder-oriented. Menlo proactively preempted the A-round.
Quote: "Menlo is Anthropic's largest institutional investor, and we are their second-largest AI investment after Anthropic." 01:58:19

Google DeepMind (AlphaProof)

Description: DeepMind's formal math AI, which achieved a silver medal (28/42) at the 2024 IMO — one point from gold.
Why mentioned: Described as a "historic moment" that opened the era of competitive AI mathematics. Started as a secret project by a single intern in 2021, scaled into AlphaProof over 3 years.
Quote: "From one intern starting secretly in 2021 to AlphaProof in 2024 scoring 28 points at IMO — one point from gold. That was a cross-century moment. Kudos to them." 01:38:04

Periodic Labs / Future House (Edison)

Description: AI for Science companies. Future House (now Edison) founded by Sam Rodriguez (MIT alum).
Why mentioned: Contrasted with Axium — AI for Science requires wet labs and physical iteration cycles; AI for Math is purely digital with instant verification. Hong respects them and envisions Axium's formal provers solving theoretical problems for AI Science companies.
Quote: "I respect my friends doing AI for Science. But if you want fast iteration with computation and logic, math and code are the better sandbox." 03:23:30

4. People Identified

Ken Ono (小野肯)

Description: Full professor (tenured) who left his position to join Axium as employee #15. Expert in number theory, partition functions, Ramanujan's work. Former VP of the American Mathematical Society, White House policy advisor, executive producer of the Ramanujan biopic.
Why mentioned: The "57-year-old tenured professor who quit to work for a 24-year-old Chinese girl" story became international news. He is the team's primary benchmark creator (adversarial problem designer) and culture carrier.
Quote: "Ken has the personality of a high school basketball coach — he keeps everyone enthusiastic and optimistic. He also intercepted an offer from OpenAI to join us." 02:15:00 and 02:11:50

Shubo (surname withheld)

Description: Co-founder of Axium. ~8-9 year Meta/FAIR veteran, Director of Facebook AI Research. One of the first CUDA developers (2014–2016). Was part of Baidu's Silicon Valley AI team alongside Dario Amodei (Anthropic) in the early days.
Why mentioned: Brought 20 years of GPU and AI infrastructure experience. Was part of the "Baidu mafia" that spawned Anthropic and much of modern AI. Met Hong by accident at a Palo Alto coffee shop over 1.5 years.
Quote: "He joined Baidu's Silicon Valley AI lab in 2015–16 because Andrew Ng said: 'You know GPUs, you know some math — that's basically AI, come join us.' Dario Amodei was in that same small team." 01:27:18

Evan Chen

Description: Coach of the US IMO (International Mathematical Olympiad) team. Described as a "gifted" competition mathematician.
Why mentioned: Present in Axium's war room during the Putnam attempt. Drew a single-diagram solution to a problem that the AI solved with thousands of lines of Lean code — illustrating the complementarity of human and AI approaches.
Quote: "Evan looked at one problem, drew a picture, and we all said 'oh, you've solved it.' The AI found no such elegant solution — it produced thousands of lines of Lean through brute-force case analysis." 02:12:45

François Chartrand

Description: AI for Math researcher. Co-authored with Mistral's Chief Scientist Guillaume Lample a 2019 paper showing transformers could outperform Mathematica on symbolic integration. Joined Axium as the 3rd employee.
Why mentioned: One of the most prolific researchers in AI for Math discovery (not just proof). His presence was a key factor in convincing Ken Ono to join Axium over OpenAI.
Quote: "François and Guillaume Lample wrote the paper showing transformers could beat Mathematica on integration. Since then, François has published paper after paper on AI solving specialized math problems." 02:13:31

Howard Morgan

Description: Co-founder of Renaissance Technologies (with Jim Simons) and First Round Capital. Still teaches at NYU. Now partner at B Capital.
Why mentioned: Led Axium's seed round. Described as a rare investor who understood the problem deeply and was more bullish on the commercial potential than the founder herself.
Quote: "Howard Morgan is a mathematician who co-founded Renaissance with Jim Simons. Talking with him was the most exciting conversation during my entire fundraising process." 01:41:31

Tao Zhexuan / Terence Tao (陶哲轩)

Description: Fields Medal winner, UCLA professor, prolific advocate for formal mathematics.
Why mentioned: His public writing and podcasts about formal proofs were a direct inspiration for Hong's decision to build Axium. He pioneered collaborative "blueprint" formalization projects (e.g., with Alex Kontorovich on the prime number theorem).
Quote: "Terence Tao has many podcasts and writings about formal proofs. My friend Kenny was one of the 5–7 students who built the foundations of Mathlib from scratch. All these people have now gathered together at Axium." 01:06:57

5. Operating Insights

Free Attention vs. Bounded Attention: The Founder's Hidden Edge

Hong describes a framework — "bounded attention" (reactive execution) vs. "free attention" (unstructured thinking) — that she learned from a mentor. She argues that the best founders are differentiated not by how well they execute tasks, but by how they protect and deploy free attention. Over-optimizing for daily execution destroys the cognitive space where strategic insight originates.

"Many successful entrepreneurs are very disciplined executors — they execute daily compound interest. But free attention is what separates an average founder from a strategic, decision-making one... When you schedule every minute for military-drill execution, you lose the opportunity cost of free attention." 01:16:35

This explains why she still walks, avoids overscheduling, and encourages wandering — it's not indiscipline, it's deliberate cognitive management.

Recruiting by Letting Great People Self-Select, Not by Pitching Them

Hong describes a consistent pattern: she did not pitch Ken Ono, Shubo, or François Chartrand. She shared progress, let them observe, and waited for them to say they wanted in. She explicitly worried that "selling" them would lead to misalignment.

"I can't convince you. You can only convince yourself. If you want to do this, and I want to do this, we can do it together. But if I start pushing you, I might be misleading you — everyone is an adult making their own interesting choices and bearing the risk of those choices together." 02:08:24

This is a non-obvious founder hiring philosophy: create a project compelling enough that top talent asks to join, rather than recruiting aggressively. The Putnam perfect score served this function — it was proof-of-concept for the team, not just a PR stunt.

Fundraising Is Iteration, Not Persuasion — And Candor Backfires Initially

Hong shared a rare honest account of how she fundraised: she presented risks and conservative projections, only to learn that VCs systematically discount everything founders say. By being honest about uncertainty, she accidentally undersold herself.

"I said our business model is not very certain. VCs are used to founders pitching optimistically and then mentally discounting everything. If you tell them '7 out of 10,' they'll discount to nothing. I learned this afterward." 01:43:56

The key corrective: find the one or two investors who are genuinely excited enough to bid against each other. The valuation tripled from first offer to final close.

6. Overlooked Insights

Transfer Learning from Math to Code Verification Is Already Working — And Is Surprising Even to Axium

This was mentioned almost in passing but is potentially the most commercially significant finding in the entire conversation. Axium's math theorem prover — trained purely on mathematical proofs — spontaneously transfers to high-performance code verification, achieving 98.93% on the Verina benchmark vs. DeepCruver's 11%.

This suggests that mathematical reasoning and formal code verification share deep structural commonality, and that a math-specialized AI may be the fastest path to industrial-grade code verification — not a code-specialized one. This is the "降维打击" (dimensional attack) strategy Hong describes: go deeper into math than anyone in code verification, then dominate code verification from above.

"We discovered that a theorem prover that solves Putnam problems transfers to strong code verification performance. On the Verina benchmark, DeepCruver scored 11%. We scored 98.93%." 01:59:42

"We believe math and code are twin siblings. Code is math because of the Curry-Howard correspondence — every mathematical proof can become a computer program." 02:30:32

The investment implication: the addressable market for formal code verification (chips, distributed systems, safety-critical software) is dramatically larger than the AI for Math market alone. If this transfer holds at scale, Axium's real TAM is the entire software verification industry — not the niche of math competitions.

The "Morgan Prize to AI" Pipeline Is Already a Recognized Talent Signal

In passing, Hong mentions that the Morgan Prize (North America's highest undergraduate math honor) has become a de facto AI talent signal. She names Levon Alpert (Anthropic) and Greg Young (xAI co-founder) as recent recipients who went directly into frontier AI.

"Morgan Prize is like a thing in AI. Levon Alpert at Anthropic, Greg Young who is an xAI co-founder — the Morgan Prize winners have been flowing into AI." 01:14:08

This is non-obvious because the prize is almost completely unknown outside academic mathematics. But it identifies the overlap of "top mathematical talent" and "likely to shape frontier AI" better than most other signals. For investors and talent scouts, tracking Morgan Prize winners (and their advisor networks at MIT, Princeton, etc.) is a high-signal, low-competition recruiting and investing channel.