Mathematical Superintelligence: Harmonic's Vlad & Tudor on IMO Gold & Theories of Everything
Summary
Harmonic’s core bet is that mathematics is reasoning, and formally verified output can turn AI capability into something users can trust. Aristotle produces annotated Lean code whose steps are checked by a small kernel against three basic axioms, subject to the crucial caveat that the kernel and theorem statement were set up correctly. The product ambition is an “amazing calculator”: frontier-model expressiveness with calculator-like reliability.
Aristotle’s gold-medal-level performance at the 2025 IMO supports Harmonic’s thesis that reinforcement learning can scale unusually efficiently around verifiable rewards. Harmonic, OpenAI, and Google DeepMind all missed Question 6, which Achim estimated was perhaps 5x harder even for humans and unusually dependent on spatial reasoning, but Harmonic saw “signs of life” from further runs. The founders expect a broadly smooth capability exponential and say Harmonic is already “punching well above our weight” relative to larger labs.
Lean 4 and Mathlib could replace substantial parts of mathematical peer review with computational certification and open-source distribution. Mathlib is framed as “every math textbook in the world merged into one in a self-consistent way,” while Lean lets contributors submit proofs through a GitHub-like workflow in which correctness is tested rather than socially conferred. Prestige could migrate from journal gatekeepers toward stars, forks, dependencies, and reuse—opening serious mathematics to contributors outside elite institutions.
Formal verification may become the control layer for AI-generated software, starting where bugs are most expensive. The founders describe API users checking cryptographic implementations for collision properties and considering whether autopilot controllers admit unstable input sequences; they also say users are using Aristotle to check safety-critical software. Longer term, the founders question why AI should write Python or Java, languages optimized for human readability. If agents can produce a roughly 1.5-million-line browser or a 5,000-page proof, manual review stops scaling, creating a path from artisanal formal methods to “formal vibe coding.”
Harmonic is using open access as both a distribution strategy and a decentralized mechanism for mathematical taste. Rather than employ an internal group to decide whether Navier–Stokes matters more than P versus NP, Harmonic exposes Aristotle through an API and web interface, letting community demand allocate compute. The founders prefer a future of millions of tool-empowered researchers over “a giant AI lab with a two-gigawatt data center” capturing every discovery and its value.
The training philosophy favors scalable search over human aesthetic supervision, while treating hallucination as necessary exploration. Harmonic has done essentially zero mathematician-panel A/B testing for elegant proofs; instead, researchers optimize what Achim called the “net present value of future proofs,” penalizing approaches that solve easy tasks through brute force but fail to build reusable competence. Pretrained models remain useful starting points, potentially complemented by higher-entropy systems less anchored to human methods: “Hallucinations are what allow a model to explore something that has never been encoded by a human before.”
The 2030 vision is theoretical abundance rather than immediate omniscience: many coherent explanations, followed by a new data bottleneck. Achim imagines perhaps five internally consistent theories unifying quantum mechanics and general relativity, with increasingly high-energy experiments needed to distinguish them—“theoretical explanations for everything,” but not knowledge without observation. Harmonic’s present Lean-only action space limits operational risk; the founders expect cybersecurity concerns to rise once such systems gain APIs and autonomy, and insist that “humans should be in charge and calling the shots.”
Deep dive
1. Mathematics is reasoning, and abstraction’s utility often arrives late
Achim’s core framing is broader than theorem proving: “mathematics is reasoning,” meaning the process of decomposing an explanation into “small sequences of logical steps” that other people can inspect. Physics, taxes, cosmology, and engineering differ in subject matter, but each ultimately requires a self-consistent account that follows from explicit facts.
Achim entered mathematics through physics, beginning with Stephen Hawking and Brian Greene before studying at Stanford. Questions about the Big Bang, gravity, and whether today’s forces splintered from “one thing at the beginning” repeatedly sent him from physics into differential geometry and pure mathematics; his practical chain is math to physics, physics to engineering, and engineering to flight, transistors, GPS, and other valuable systems.
The “unreasonable effectiveness of mathematics” supplies Harmonic’s answer to demands for immediate utility. Abstract work on manifolds later became essential to relativity, while number theory went from an esoteric pursuit to a foundation for the secure digital economy. Achim’s prescription is consequently portfolio-like: “You just do the math,” knowing some fraction will become more useful than anyone initially imagined.
The founders distinguish rare, artist-like mathematicians who produce a major new idea every five to ten years from prolific synthesizers who absorb papers, remember techniques, and transfer them across fields. AI may eventually accelerate the former, but GPT-4 already suggested leverage on the latter: searching vast literatures, retrieving the relevant trick, and combining knowledge faster than any individual reader.
2. Lean turns a proof into an executable certificate
Achim calls Lean “the best programming language ever created” because it spans ordinary programs and logical claims. As a dependently typed language, it can express complex properties at compile time rather than merely run code and inspect the result; in his spectrum, JavaScript checks almost nothing, while Lean can specify and verify unusually rich invariants before execution.
Lean rests on the calculus of constructions plus three axioms: propositional extensionality, quotient soundness, and the axiom of choice. The last says that an element can be selected from a nonempty set; all three are short enough to fit within a tweet, and the founders argue that this minimal base can support mathematics, computer science, and quantitative modeling across physics, economics, statistics, and biology.
Nathan Labenz’s chess analogy survives intact: a theorem says that a starting board can reach a target board, while its proof lists the intervening moves. Lean’s kernel checks each claimed move against its rulebook and verifies that the final state was reached. The moves are mathematical rather than chess moves, but the certificate carries the same structure: “This step is right” repeated until the destination.
The learning curve can begin below research mathematics. Achim recommends the Natural Number Game, where users derive properties of addition and multiplication, and points to a real-analysis game that progresses from sequences and real numbers toward calculus foundations. His larger prediction is that mathematics education will migrate from the chalkboard toward the computer lab, potentially reaching middle-school students.
3. Mathlib could move mathematics from journals to GitHub
Tenev remembers doing his late-2000s mathematics almost entirely on chalkboards, whiteboards, and couches, using computers mainly to typeset completed work. Lean relocates the working process into VS Code, Cursor, and GitHub, enabling geographically distributed collaborations in which dozens of people can formalize research or attack a project such as Fermat’s Last Theorem together.
Mathlib supplies reusable higher-level moves above Lean’s small kernel. Organized across algebra, geometry, real analysis, statistics, and other fields, it consolidates definitions and proven results that can be invoked like functions from a software library. Achim’s endpoint is “every math textbook in the world merged into one in a self-consistent way,” rebuildable from foundations on an ordinary computer.
Formalization changes trust, with two caveats preserved: the Lean kernel must be bug-free, and the theorem must faithfully state the intended claim. Within those constraints, a checked proof no longer needs a prestigious mathematician to vouch for every step. A “citizen mathematician” can contribute a certificate without persuading an elite department or journal to establish its correctness.
Achim compares the transition to open-source software’s move from the “cathedral” to the “bazaar.” Anyone could submit a proof; Lean would test correctness, maintainers could judge style, and stars, forks, dependencies, and reuse could measure impact. The timing mattered: Lean 3 still felt like beta software, while Lean 4 and GPT-4 became practically useful around Harmonic’s 2023 launch.
4. Aristotle searches at several scales rather than merely grinding
Labenz decomposes the IMO-era system into Monte Carlo tree search, an informal lemma generator, and a geometry specialist, but Achim corrects the idea that tree search is merely brute force. Its language models infer consequential high-level steps and solve difficult subproblems; only deep in the tree does the work become routine case-closing.
The search machinery itself is built from LLMs: one component proposes steps, another scores them, and they work together on lemmas before assembling a complete Lean proof. The informal reasoner is best understood as context management, not as an infallible guide to base camps. It produces “enormous quantities of mistakes,” including proposals that may be wrong or impossible to formalize, from which useful waypoints can nevertheless emerge.
The geometry module is closer to a true grinder. Labenz compares it to AlphaGeometry; Achim says it explores high-level steps and then uses an algorithm to grind through the consequences. Geometry fell relatively early because, as Labenz notes, its objects and relationships are constrained—points yield only so many angles—though the search space still explodes once a diagram contains ten or fifteen points.
Two less conspicuous components carry substantial product value. Autoformalization translates natural-language prompts faithfully into Lean, while theory building creates structures not already present in Mathlib and incorporates them during proof search. Achim cautions that the architecture has already been substantially consolidated and revised since the IMO system; the technical report describes a moving snapshot, not a fixed product.
5. Provability ends where people cannot agree on valid reasoning
Labenz stress-tested informal mode with intentionally awkward prompts. Asked to prove “all is love,” Aristotle classified the proposition as philosophical and outside Lean 4’s scope; asked to prove “Epstein did not kill himself,” it treated the statement as a question about current events rather than a formal theorem. The refusals exposed the harder step preceding proof: deciding what proposition faithfully represents a messy real-world claim.
Achim places the eventual boundary wherever people can agree on what constitutes a valid sequence of reasoning. Mathematics and chess fit immediately; quantitative software behavior also fits because inputs, branches, loops, and outputs imply checkable relationships. He is less convinced that history essays will become objectively verifiable, tentatively limiting the target to “anything that’s quantitative and logical in nature.”
Existing API usage illustrates the software extension. A cryptographic implementation can be checked for whether two inputs might collide when the algorithm requires uniqueness; an autopilot controller can be tested symbolically for an input sequence that creates an unstable dead zone. Unlike unit tests, which sample executions after code exists, formal reasoning can seek to establish behavior across all inputs satisfying stated assumptions.
Tenev takes the broader side of the founders’ disagreement. An early Aristotle could invent a theory around “all is love,” and users have already submitted biology, medicine, economics, and financial-mathematics questions; current restrictions mainly steer customers toward reliable value. He can imagine internet facts becoming explicit axioms, while astronomy questions—such as the next total eclipse within 50 miles of Palo Alto—already show why first-principles calculation beats retrieval.
6. Community demand, not an internal panel, supplies mathematical taste
After IMO gold-level performance, Harmonic faced a choice: keep Aristotle internal, recruit elite mathematicians, and periodically announce private accomplishments, or expose it broadly. The company chose APIs, a terminal interface, and then a web interface, letting the community’s “revealed preference” determine which problems deserve compute instead of declaring Navier–Stokes more important than P versus NP.
That choice surfaced work Harmonic would not have prioritized internally, including computational learning theory, graph conjectures, computer science, cryptography, and branches of number theory. Tenev frames the strategic fork starkly: discoveries can emerge from a two-gigawatt lab that captures the value, or from millions of empowered people who work independently, collaborate, receive credit, and retain more of the upside.
Labenz presses on a different kind of taste: whether Aristotle’s proofs are elegant rather than merely correct. Harmonic has conducted essentially zero proof A/B testing through panels of mathematicians. Achim instead describes the objective as the “net present value of future proofs”—favoring methods that minimize the future computational cost of solving increasingly difficult problems, not those that merely impress a human reviewer today.
That objective contains a deliberate tension. Brute force may produce a short-term efficient answer on easy problems, yet teach nothing reusable and become expensive later; among genuinely reasoned solutions, shorter and more efficient proofs are preferred. Harmonic follows the “bitter lesson”: start from pretrained models when useful, impose few priors, scale reinforcement learning, and potentially mix in higher-entropy systems less biased toward established human mathematics.
7. Verifiable output substitutes for understanding the model’s internals
Labenz asks whether interpretability could reveal new abstractions inside a mathematical model, or whether Aristotle might eventually merge with a fuzzier world model—his playful endpoint is a benevolent, “safe HAL 9000” operating a spacecraft. The underlying concern is that correctness certificates may reveal what a model proved without explaining how its internal representations generated the insight.
Achim responds that interpretability is often sought as a proxy for trustworthiness, which Harmonic addressed at the beginning of the company by requiring formal output. Lean is the “most interpretable possible output”: a machine checks it, while a human can repeatedly use “go to definition” and traverse the proof like a codebase. The model may remain mechanistically opaque, but its externally consequential reasoning is inspectable and certified.
Harmonic has therefore prioritized cheap, verified proofs over opening the neural network. One founder suggests—while conceding “I might be wrong”—that the more comprehensible route may be to study how Aristotle combines techniques from three mathematical subfields in an unprecedented solution. That behavior-level account could be more useful than excavating weights for an internal “spark of superintelligence” they have not yet observed.
8. IMO gold coincided with a phase transition from informal to formal
Harmonic, OpenAI, and Google DeepMind all reached gold-medal-level performance on the 2025 IMO and all missed Question 6. Achim estimates that problem may be 5x harder even for humans, with many steps and spatial reasoning that is difficult to encode formally. Continued runs produced “signs of life,” so he regards its eventual solution as plausible rather than evidence of an architectural wall.
Questions 3 and 5 would likely have exceeded most models only a year earlier, reinforcing the founders’ view of a roughly smooth exponential. Community workflows are also becoming compositional: Labenz has seen GPT-5.2 Pro generate a candidate proof in token space, followed by Aristotle formalizing and checking it. Separately, Aristotle users have solved hard-ish problems that had remained open for 30 or 40 years.
Achim sees the discontinuity elsewhere: a “phase transition to formal” has already occurred. Work that mathematicians recently considered laughable—uploading a full number-theory paper and automatically translating it into Lean—now works through repeated Aristotle runs. Harmonic has even considered a “Ralph button” that simply keeps the system going until formalization finishes, leaving humans to select problems and evaluate techniques rather than check every deduction.
Scale makes the founders categorical about the destination. Nobody will manually review a 5,000-page proof, much less the hypothetical 100,000-page Riemann-hypothesis attempt that motivated Harmonic in 2023. Labenz notes that DeepMind moved from formal AlphaProof in 2024 to informal Gemini this year, while OpenAI’s IMO system was informal; training may remain hybrid, but Harmonic considers the formal-versus-informal output debate “settled.”
9. AI-written software creates the same verification bottleneck as AI mathematics
The founders extend the long-proof argument directly to code. The Cursor team’s experiment generated a Chromium-compatible browser of roughly 1.5 million lines; as agents work autonomously for weeks, neither humans nor collaborating models can economically inspect every line for vulnerabilities. Verification cost must grow much more slowly than generated complexity if such systems are to become dependable infrastructure.
Tenev questions whether AI-generated code should remain in Python or Java, which were designed partly for human readability. If machines are the principal authors, formally verifiable languages may offer a better target because properties can be established rather than inferred from tests and code review. Lean is Harmonic’s favorite language, though the founders acknowledge that adoption remains an open question.
Diffusion should begin with mission-critical systems, where defects are unusually costly and teams already hire Lean, Rocq, or Isabelle specialists for painstaking verification. Aristotle can first accelerate those experts, then broaden the practice toward “formal vibe coding.” The envisioned endpoint is not merely faster programming but increasingly bug-free software whose security and safety claims carry machine-checkable certificates.
10. New abstractions require entropy, not escape from logic
Labenz’s sharpest metaphysical pushback asks whether training inside today’s formal system traps AI inside today’s abstractions. Einstein overturned the intuitive three-dimensional worldview, so perhaps mathematical superintelligence must similarly “break the fourth wall.” Achim’s answer is that Einstein could still express the breakthrough rigorously through differential geometry; any new theory that proceeds through independently checkable deductions can itself be encoded in Lean.
Lean’s axioms are intended to describe extremely minimal reasoning operations, not a particular physical paradigm. Achim therefore treats formal reasoning as an especially detailed, computer-checkable version of informal reasoning rather than a conceptual cage. Gödelian incompleteness leaves true but unprovable and undecidable statements at the frontier, but the founders do not expect those edge cases to prevent proving “the lion’s share of useful things.”
Entropy remains essential inside that framework. Aristotle tries many paths that fail, and those failures enable it to reach ideas never written by a human; “hallucinations are a key part of a reasoning system.” The desirable design is not a hallucination-free generator but a high-entropy explorer coupled to a formal verifier—able to pose false statements, discover they are false, and retain only certified conclusions.
11. The endgame is theoretical abundance constrained by experiments
Harmonic’s stated trajectory runs from its 2023 founding to 2025 IMO gold-level performance, a topped year-end benchmark, and API users solving hard-ish problems that had remained open for 30 or 40 years. The next flywheel is straightforward: autoformalization expands Mathlib, a larger certified library makes harder proofs cheaper, users pursue more important conjectures, and near-daily product improvements reduce the friction and cost of submitting work.
Achim’s 2030 asymptote is “theoretical explanations for everything basically.” Rather than struggle to find any coherent bridge between quantum mechanics and general relativity, science might possess five competing unifications that fit all available observations. The bottleneck would then return to data: researchers would need increasingly high-energy experiments and perhaps new colliders to discover which mathematically consistent account describes the actual universe.
The claim is explicitly not omniscience. Models can reason only from grounded assumptions and observations; some properties of the universe “you just have to run the experiment and find out.” Yet Achim expects enormous utility before the asymptote: removing the shortage of people capable of sustained high-level logical reasoning could create a scientific renaissance.
Safety today comes partly from constrained action space: Aristotle emits Lean files rather than autonomously reaching into Gmail, iMessage, or operational systems. Tenev expects the first serious risks from more connected agents to resemble cybersecurity incidents created by APIs and autonomous execution. As Harmonic eventually connects its models to the world, Achim says the company will need to take those risks much more seriously, while preserving their governing principle: “Humans should be in charge and calling the shots.”