Mathematical Superintelligence

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.”

🔗 Original source & video: Mathematical Superintelligence: Harmonic’s Vlad & Tudor on IMO Gold & Theories of Everything