AI brute-forces a Putnam problem with thousands of lines of Lean code, and that is not a victory for intelligence
The Putnam competition has produced only five perfect scores in 98 years. AI just got the sixth — but it did not walk the human path. It enumerated its way through thousands of lines of Lean code. Automated theorem proving existed long before AI.
The video won't play here. Listen to the audio instead:
The argument · tap a timestamp to hear it
AI got a perfect score without walking the human path
Axiom's Action Prover scored a perfect score on the Putnam Competition, the university-level math contest. The competition began in 1927, and in the past 98 years only five humans have ever scored perfect — this is the sixth, earned by AI. The interesting part is the comparison of solutions: Evan Chen, the coach of the US IMO team, drew a single diagram and solved one of the problems. The AI never found that solution. Instead it used thousands of lines of Lean code, grinding it out step by step through something like enumeration and case analysis. Hong Lezhong calls this ‘brute force that produces miracles’ — even for a problem that clearly admits a creative solution, the machine will take the path it is good at and produce a completely different solution.
— Hong LetongAutomated theorem proving is not a victory for AI
Hong corrects a common misunderstanding: the field of automated theorem proving (ATP) existed before deep neural networks, before AI. It was a group of computer scientists hoping to use rule-based systems to help humans solve mathematical problems. ITP is interactive theorem proving, historically done by human mathematicians working in cooperation with computer systems. What is happening now is simply replacing the human in ITP with AI. So this old discipline is essentially the intersection of ATP and AI, and it cannot be counted as a victory for AI.
— Hong LetongThe ratio of bounded attention to free attention
Hong's advisor proposed a pair of concepts: bounded attention is attention that is framed, like the emails and deadlines you must process every morning; free attention is free attention, and many successful entrepreneurs are extremely disciplined executors, compounding execution day after day. But what distinguishes an average founder from one who makes strategic decisions is precisely free attention. She stresses this is not linear — time put into free attention may produce nothing at all, but later, when forced to do tasks, there is a callback, a return to the foundation that free attention laid down for the brain. The ratio varies from person to person; she does not know her own.
— Hong LetongJumping from constitutional interpretation to AI doing math
While studying constitutional interpretation in law school, Hong encountered three interpretive approaches — originalism, textualism, living constitutionalism — and she considers herself a textualist. Someone suggested feeding language models data like the founding documents to understand word meanings, and from that she thought: if AI can already see what the Constitution means, why can't AI do mathematics? Because mathematics does not need English; it needs a more structural presentation, and formal languages turn mathematics into code. One of her best friends, Kenny Law, has been doing Lean formal proofs since 2020, is one of the earliest five to seven builders of Mathlib, and is a student of Kevin Buzzard.
— Hong LetongA mathematician background may be a demerit for a scaling team
Axiom set a rule early on: do not hire mathematicians until the 15th person, because the seed round was an under-raise relative to what they wanted to do, and headcount was constrained. More critically, some classmates with mathematics backgrounds were hesitant about scaling, or even disliked the philosophy, feeling that mathematics is a craft, like a Japanese master shaping sushi. Some accepted an offer and then did not come, saying they did not want to work on an Internet Scale Dataset. So now hiring mathematicians requires very open-minded thinking; they want them to do adversarial benchmark creation, working against the system, to feel where the system is weak. After Ken Ono joined, he became the number one figure in the benchmark-level assembly.
— Hong LetongFundraising is a group game; nobody wants to reject first
Hong describes investors' real behavior during fundraising: they do not reject you directly, they stall you — because they fear that after rejecting you, you will ignore them later, so they wait for you to get someone else's offer and then follow. She calls this mechanism groupthink. So what the founder really has to solve is not ‘convincing everyone’ but finding a lead investor willing to say yes first; the rest will oversubscribe. In her seed round she got three lead offers at the same time, and the price went from one times to two times to three times, one step up per month.
— Hong LetongLean data is scarce, so you have to build your own verification tools
Lean is a formal language, and the total number of tokens in the public domain is very small, nowhere near comparable to Python. It is simultaneously a programming language, a compiler and a runtime, and it is very finicky — objects must satisfy all sorts of constraints. She also points out the cheating risk: if you assume the axiom that n plus n equals n, you can ‘prove’ that 2 plus 2 equals 2. The comparator the community used before was a hundred times slower than their in-house verify proof, so they built twelve or thirteen auxiliary tools. AlphaProof uses Monte Carlo tree search; they felt it was too expensive, they did not have the money, so they had to find another way.
— Hong LetongTranslating mathematics into Lean is harder than proving
She believes auto formalization is severely underestimated: converting paired theorems and proofs from arXiv papers into Lean code requires first extracting a blueprint, and a 20-page article may expand into 200 to 500 pages. Terence Tao, Kevin Buzzard and Alex Kontorovich once wrote blueprints by hand, then distributed them to undergraduates around the world, each taking a small piece. She points out this is not translation — English and French have similar levels of abstraction, whereas Lean is more like Python, and AI has seen very little Lean data. The reverse direction, auto-informalization, is easier, but you need cycle consistency to repeatedly convert back and verify correctness.
— Hong LetongIn their own words · checked verbatim
In 2024, AlphaProof came out of nowhere and got 28 points, a silver medal one point short of gold. For me that was the moment IMO was solved.
2024一炮而同的这个Alpha proof 拿了28分差一分金牌的银牌 这个对我来说是一个 是IMO被解决的那一个时刻
Hong Letong1:37:43
It is just tiring. You are a repeater. Over and over you say the same thing, over and over you get the same question.
它就是累 你是一个复读机 你一次一次的 说一样的事情 你一次一次的 接到一样的问题
Hong Letong1:40:43
Being young and doing product is a plus. Being young and doing deep tech is a minus.
年轻做product是加分 年轻做deep tech是减分
Hong Letong1:50:45
People have not realized one thing: we are not a model company. We are a deep tech company. What we are doing is a bit like SpaceX.
大家没有意识到一件事情 我们不是一个模型公司 我们是一个deep tech公司 我们是一个深科技公司 我们做的这件事情 有点像spacex
Hong Letong2:02:48
Now is not the moment for the pure beauty of mathematics. Do not go precisely fiddling with these things. Now is a state of war.
现在不是说数学纯粹之美的时刻 不要去精确的去搞这些东西 现在是战争状态
Hong Letong2:22:05
But if you merely take mathematics that humans have already discovered and written down and convert it into this formalized form, you will get less praise. Yet this technology is actually harder than the proof, at least equally hard — I actually think it is harder.
但是如果你只是把 这个人类已经就是发现了的 写好了的数学 转化为了这个形式化的 你会得到更少的赞美 但是这个科技 它其实比这个证明要更难 至少是一样的难度 我其实觉得是更难
Hong Letong2:46:31
Figures
| Putnam Competition AI perfect score | the 6th perfect score in human history (5 since the contest began in 1927) | 12:04 |
| Alpha Geometry share of IMO geometry problems solved | 81% | 10:03 |
| Axiom team size after seed round | 30 people | 1:28:37 |
| Axiom funding valuation | $1.6 billion Series A | 0:00 |
| Seed round valuation | $300 million | 1:48:44 |
| Series A valuation | $1.6 billion | 1:59:47 |
| Series A funding amount | at least $200 million | 1:59:47 |
Glossary
- ATP / Automated Theorem Proving
- Using rule-based systems to prove mathematical theorems automatically; it predates deep learning.
- ITP / Interactive Theorem Proving
- Human mathematicians and computer systems cooperating to complete proofs; now the human is replaced by AI.
- Lean
- A formal mathematics language that is simultaneously a programming language, a compiler and a runtime.
- auto formalization
- Converting natural-language mathematics papers into Lean code; harder than the proof itself.
- groupthink
- Investors watch each other and avoid rejecting first, waiting for someone else to move before following.
How to listen
Founders doing deep tech or AI for Science, investors watching early-stage fundraising games, and engineers who want the frontier of formal mathematics meets AI.
If constitutional interpretation and founder taxonomy do not interest you, skip the segments at 1:04:26 and 18:05.