Descriptions:
Cognitive Revolution host Nathan Labenz sits down with Vlad Tennv and Tudor Rake, co-founders of Harmonic, to discuss Aristotle — the AI system that achieved gold medal performance at the 2025 International Mathematical Olympiad. Unlike OpenAI and Google DeepMind’s IMO-level systems, which scale reasoning through chain-of-thought, Harmonic’s approach is built around formally verifiable proofs generated in Lean 4, a proof-checking language whose trusted kernel validates every logical step from explicit axioms. Aristotle’s outputs can therefore be automatically verified rather than evaluated by human judges, and its performance ceiling is theoretically bounded only by available reinforcement learning compute.
The interview covers the full architecture in detail: a large transformer backbone using Monte Carlo tree search (echoing AlphaGo) to explore mathematical reasoning paths, a lemma-guessing module that generates intermediate waypoints to help manage long-horizon proofs, and a specialized geometry module modeled on DeepMind’s AlphaGeometry. The conversation also addresses Aristotle’s informal API mode, which attempts to autoformalize natural-language problem statements before proving them — and what its responses to philosophical edge cases reveal about the hard boundary between provable mathematical statements and empirical or interpretive claims.
Looking further out, the co-founders describe a future of “theoretical abundance” where all known mathematical results live in Lean’s Mathlib — a single machine-verified, searchable repository checkable from axioms with one build command. Applications discussed include hardening mission-critical infrastructure, accelerating open mathematical research, and building a form of superintelligence whose outputs can be trusted even in the absence of mechanistic interpretability.
📺 Source: Cognitive Revolution “How AI Changes Everything” · Published February 18, 2026
🏷️ Format: Interview
