Three IMO Golds Missed the Same Problem. Harmonic Wants Math to Compile

In 2025, three AI labs announced International Mathematical Olympiad gold-level performance: OpenAI, Google DeepMind, and a much smaller research lab called Harmonic. OpenAI and DeepMind got there by scaling chain-of-thought reasoning. Harmonic's system, Aristotle, generates candidate proofs in Lean, a programming language whose trusted kernel checks that every step follows from a few explicit premises and accepted logical rules. Host Nathan Labenz notes that, in principle, Aristotle's performance is then limited only by the compute available for reinforcement learning.

The guests are Vlad Tenev and Tudor Achim, Harmonic's co-founders. The conversation is unusually metaphysical for the show, but the practical stake is clear: they want verifiable reasoning that can harden software, change how mathematics is done, and, they hope, produce a superintelligence whose outputs you can trust even if you never understand the model's internals. Labenz flags one later result up front that will matter for the rest of the hour. When the three gold-level systems are compared, they all missed the same contest problem.

Achim's definition is deliberately plain. Mathematics, he says, is the process by which humans understand the world by breaking that understanding into small sequences of logical steps that other people can verify. Solving a physics problem, doing your taxes, or thinking about the beginning of the universe all end in the same demand: a self-consistent explanation that follows from other facts and that colleagues can check. Being good at math, on this view, is being good at that decomposition. Group theory and the blackboard scenes from *Good Will Hunting* are the costume; reasoning is the thing itself.

Tenev arrived at the same place through physics. At Stanford he had read Brian Greene's *The Elegant Universe*; as a child, one of the first English books he finished was Hawking's *A Brief History of Time*. He wanted to know what happened before the Big Bang, and whether gravity, electromagnetism, and the strong and weak forces had once been a single force that splintered as the universe cooled. Every time he pushed the physics department far enough, they sent him to mathematics: string theory and general relativity both required differential geometry. The PhD that followed was pure math, but the impetus was the real world. Flight, rocketry, transistors, and GPS are physics inventions; math is how you get there.

Achim cites Eugene Wigner's essay on the unreasonable effectiveness of mathematics. Einstein's relativity leaned on nineteenth-century thought experiments about manifolds that, at the time, looked almost preposterous as descriptions of the three-dimensional world, then turned out to be the right language once time and curvature entered the picture. Number theory spent years as the famously useless branch and then became the foundation of a secure digital economy. The moral, Achim says, is not to demand an application up front. You do the math; some of it will later be more useful than anyone imagined. Investing in the field is therefore also an investment in a stock of new mathematics to apply later.

Mathematicians, Tenev adds, already come in two tempos. Some are closer to artists, producing a new idea every five or ten years—he mentions Grigori Perelman. Others are synthesizers who read more papers per unit time, reuse tricks, and transplant them into new domains. Harmonic is excited about AI accelerating the first kind eventually, but the second is what models were already good at when the company was founded. GPT-4, which had just appeared, excelled at needle-in-a-haystack retrieval across literature. Even without a eureka machine, knowing all the relevant math for an open problem is already a superpower.

Achim calls Lean the best programming language ever created: you can write anything you would write in Python, C, or C++, and you can also express essentially any logical concept. It is dependently typed, so complicated properties of a program can be checked at compile time, before it ever runs. JavaScript sits at one end of that spectrum, checking almost nothing; Lean sits at the other. When Aristotle emits a result, it comes out as annotated Lean—theorems, programs, and comments a human can read.

Proofs in that language depend on three axioms on top of the calculus of constructions. Two are highly technical: propositional extensionality, and something about quotient soundness. The third is the axiom of choice: if you have a non-empty set, you can pick an element. It sounds like common sense and historically was not treated as such. Each axiom, written as a mathematical statement, fits in less than a tweet; the axiom of choice in Lean is about ten characters, the others perhaps a hundred. From those three, Achim says, you can build all of mathematics, computer science, and mathematical modeling in physics, economics, statistics, and biology.

Labenz asks for an analogy despite usually banning them. Achim's chess picture is the one that sticks: a theorem says that from this board you can reach that board; a proof is the list of moves; the kernel checks each move against the rulebook and confirms you arrived. Mathlib, the open-source library on top of that tiny, heavily audited kernel, is the opening book and the endgame tablebase at once—an amalgam of the world's textbooks, self-consistent, searchable, with "go to definition" all the way down. Tenev notes that Lean 4 shipped in roughly the same month as GPT-4, which was also the month Harmonic launched. Both tools had just become real enough to combine.

The social change, Tenev says, is already here even if you subtract AI. In his late-2000s PhD, thinking happened on a chalkboard and collaboration happened in an office or at a conference; the computer was for typing up the paper. Lean moved mathematics into VS Code and Cursor and onto GitHub, where famous mathematicians now run projects with dozens of collaborators, including a formalization of Fermat's last theorem. If the proof checks, and there is no bug in the kernel or in how the statement was posed, manual human verification becomes unnecessary. Achim compares it to open source: a pull request that passes tests can merge without anyone knowing you, and prestige becomes stars, forks, and dependency graphs. Lean is the computational certificate that lets math go from cathedral to bazaar.

The IMO-era Aristotle had three parts, which Achim says have since been consolidated and improved. The first is Monte Carlo tree search, which Labenz analogizes to AlphaGo: explore branches, score them with a learned function, go deeper where the path looks promising. Achim pushes back on calling that a mere grinder. The lemmas at this level are closer to "solve a hard contest problem" than to "prove two squared equals four," and only the bottom of the tree, closing easy cases, looks like grind. Language models both propose steps and score them.

The second part is a lemma-guessing module, described in the technical report as an informal reasoning system. Labenz hears "give me a mountain, guess the base camps." Achim accepts the metaphor and then undercuts the flattery: the system makes enormous quantities of mistakes, and you should not picture a smart human marking a route. It proposes ideas that need not be formalizable or even correct; you assemble what you can. One job is context management. When you focus on a small step, you should not have to hold the entire large-step context in view. Autoformalization—faithful translation from natural language into Lean—and on-the-fly theory building, creating structures that are not yet in Mathlib, are further pieces they consider independently important.

The third part is a geometry module modeled on DeepMind's AlphaGeometry. Geometry falls early, Tenev says, because it is constrained: three points imply only so many angles, and by the time you have ten or fifteen points the search explodes for humans too. Achim calls this the real grinder: it enumerates possible conclusions from a diagram, with little pattern-recognition intelligence. Labenz also tried informal mode, asking Aristotle to prove "all is love" and that "Epstein did not kill himself." The product now replies that these are philosophical or current-events claims outside the Lean 4 kernel. Tenev says an earlier version would happily have built a theory and proved the love slogan; they narrowed the surface so users would find, faster, what the tool is actually good at.

The interesting boundary, Achim argues, is any domain where people can agree on what a valid sequence of reasoning steps would be. Software is the obvious expansion: engineers already reason about loops and branches the way they reason about math, and API users are checking cryptography for colliding outputs and autopilot controllers for unstable dead zones. Entropy stays in the loop on purpose. "Hallucinations are a key part of a reasoning system," Achim says later; they are how a model explores something no human has encoded. Aristotle made many mistakes on the IMO and tried many dead paths, and that exploration is what eventually found the answers. Seeking a hallucination-free LLM, in this view, does not make much sense unless you pair the generator with a verifier. Tenev adds that the most creative humans are often the ones who hallucinate the most.

IMO gold forced a product decision. One path was to keep Aristotle in house, recruit mathematicians, and periodically announce that the system had finished X, Y, and Z. The other was to open an API and a web interface and let revealed preference decide. They chose the second. Harmonic does not declare Navier-Stokes more important than P versus NP; mathematicians with API credits do. The result has been heavy use in computer science, cryptography, and some number theory, plus a stretch of graph-theory conjectures. Behind the choice is a picture of the future: either a two-gigawatt lab captures every discovery, or millions of people work with the tools, collaborate, and keep the credit. Tenev is betting on the second, and calls the first dystopian.

Labenz asks whether training includes a panel scoring proofs for elegance. Achim's answer is that in two years they have done essentially zero of that. The metric is the net present value of the computational cost of future proofs. Early in reinforcement learning you can brute-force easy problems, but those habits hurt you later; given two non-grinding proofs, you prefer the shorter one. The tension is real, and researchers strike it by intuition, but they try to give the system as few priors as possible and run RL at scale. They believe the Bitter Lesson. Pretrained models are a fine starting point for that objective; mixing in higher-entropy reasoners not trained on human math is something they play with, not yet a limiter.

What the community actually submits looks less like contest problems and more like engineering. People verify cryptographic implementations and ask whether two inputs could collide. People verify autopilot controllers and ask whether some input sequence creates an unstable dead zone. Achim's point is that this is the same activity as mathematics. Tenev had expected a narrower use case; Erdős problems and computational-learning-theory formalizations showed up anyway, and he says they were never going to run all of that in house. Open access, in his telling, is both strategy and the world he wants to live in.

All three gold-level labs missed IMO Question 6. Tenev was not shocked: the item is perhaps five times harder even for humans, with many steps and a kind of spatial reasoning that is still difficult to encode formally. They saw "signs of life" while running on it, and he expects the problem to fall the way questions that looked unreachable a year earlier already have. The capability curve, both founders say, looks like a smooth exponential, not a wall that demands a new architecture at each band of difficulty.

The phase change Achim wants highlighted is not capability but formality. A few years ago, automatically formalizing a number-theory paper in Lean, Rocq, or Isabelle would have been laughed out of a room of mathematicians. Today people paste a full paper into Aristotle, run it a few times—they have joked about a button that just keeps going—and get a formal version. Humans stop being the verifiers and become the taste-makers: which problems, which techniques. DeepMind had started formal with AlphaProof's 2024 silver and then returned to informal Gemini for 2025; OpenAI was informal. Harmonic considers that debate settled.

Tenev's five-year picture is the reason. If autonomous math goes from five-to-ten-page proofs to 5,000-page proofs, nobody reads the output. Validation time cannot be allowed to grow linearly with complexity. That was Harmonic's founding thought experiment in 2023: ask a model for the Riemann hypothesis in ten years and you get 100,000 pages you should throw away, both because there is probably a mistake and because you cannot hold it in your head. Formal output made the math digestible and highly certain, and it also made reinforcement learning more efficient—which is how a much smaller lab punched above its weight at the IMO.

The same logic, they argue, applies to software. When agents can spend a week writing a project—Achim cites a Cursor experiment that produced a Chromium-compatible browser of about 1.5 million lines—who reads it for vulnerabilities? Python and Java are languages optimized for human readability; if AIs are the authors and the checkers, you want the cost of verification as low as possible. Mission-critical domains already hire Lean, Rocq, or Isabelle experts to formalize by hand. AI will accelerate those people first, then diffuse. Tenev expects "formal vibe coding" before long. Labenz notes that Kathleen Fisher and AWS's Byron Cook have been describing a similar path from verified infrastructure outward.

Asked what the system is doing in 2030, once Millennium Prize problems are gone, Achim answers in a way that briefly leaves Labenz without a follow-up. By 2030, he says, we will have theoretical explanations for everything, basically. Science historically leaps when new intellect or new data arrives: the microscope unlocked biology, the electron microscope unlocked chemistry. The present bottleneck is a shortage of people who can reason at the level needed to unify general relativity and quantum mechanics. Anything that can be posed mathematically—the substrate of science—should get self-consistent theories. Then the world becomes data-limited again: perhaps five unifications, all fitting existing evidence, and a wait for higher-energy colliders to tell them apart.

Labenz restates it: multiple grand unified theories, then experiments decide. Achim agrees. AI is not omniscient; it can reason about what it can ground in its own deduction rules, and some parts of the universe you simply have to measure. He adds that a great deal of utility arrives before that asymptotic endpoint. Einstein's leap, in this telling, is not a counterexample to formality. Relativity was written rigorously in differential geometry; any future theory that can be explained as a checkable chain of deductions can be encoded in Lean. Gödelian incompleteness and undecidable statements are acknowledged as edge cases that do not stop the lion's share of useful work.

On safety, Tenev is not very worried yet, because the outputs are constrained. Aristotle does not fire a request at your Gmail or iMessage APIs; it emits Lean files. The first serious dangers, he thinks, will look like cybersecurity incidents: models that call APIs, run autonomously, and both create and exploit holes. Harmonic will have to take that much more seriously when the interface is no longer a Lean file. Achim's interpretability answer sits underneath. Many people study internals as a proxy for trust. Harmonic chose, at the start, to output formally verified reasoning—the most interpretable math you can emit, navigable like a codebase via "go to definition." How the model is so smart can wait; trust is solved at the interface.

Tenev's closing value is that humans should stay at the center: accelerate the work, but keep calling the shots, which is why the tools go into many hands instead of a lab that runs in secret and makes proclamations. Achim's practical invitation is simpler. If you have never used a system whose output is always correct, sign up; the account is free. Do not ask it for 2+2, which is already a theorem in Mathlib. Try a boundary condition from your own code, or the Natural Number Game, which teaches Lean by proving that addition commutes, using those same three axioms and no research-math background.