Digest

This episode features Vlad Tenev and Tudor Akim, co-founders of Harmonic, discussing their AI research lab focused on building mathematical superintelligence. They introduce Aristotle, an AI system that achieved gold medal performance at the 2025 International Mathematical Olympiad. The conversation delves into the nature of mathematics, the power of formal verification languages like Lean, and how Lean is transforming mathematical peer review. Aristotle's architecture, including its use of transformer models, Monte Carlo tree search, and specialized modules, is explained. Harmonic's future plans involve hardening critical infrastructure and developing trustworthy superintelligence. The speakers explore the definition of mathematics, the cognitive skills involved, and compare them to LLM performance. They also discuss the "unreasonable effectiveness of mathematics" and AI's role in accelerating mathematical discovery. Lean is presented as a tool for rigorous, step-by-step reasoning, with Mathlib serving as a vast repository of formalized knowledge. The episode touches on the challenges of AI training, the importance of "taste" in AI development, and the potential for AI-driven scientific discovery by 2030. Concerns about AI safety and the vision for human-centric AI progress are also addressed, emphasizing the need for formally verified software and AI systems that remain accessible and beneficial to humans.

Outlines

00:00:00

Introduction and Sponsor Message

The episode begins with a welcome and an introduction to the presenting sponsor, Granola, highlighting its utility in identifying overlooked aspects of calls and improving team execution through follow-through on commitments.

00:01:06

Introducing Harmonic, Aristotle, and the Power of Formal Verification

Guests Vlad Tenev and Tudor Akim, co-founders of Harmonic, are introduced. Harmonic is an AI research lab focused on building mathematical superintelligence, and they are the creators of Aristotle, an AI system that achieved gold medal performance at the 2025 International Mathematical Olympiad. The discussion delves into the metaphysical nature of mathematics, what mathematicians do, the assumptions behind Lean verification, and how Lean is revolutionizing math by potentially eliminating traditional peer review.

00:02:21

Aristotle's Architecture and Capabilities

The architecture of Aristotle is explained, including its use of a large transformer model with Monte Carlo tree search, a lemma guessing module, and a specialized geometry module. Its informal mode and ability to attempt auto-formalization are also touched upon.

00:03:20

Future Plans, Societal Impact, and Defining Mathematics

The conversation shifts to Harmonic's future plans, the community's use of Aristotle, hardening critical infrastructure, improving complex systems, and the potential for a trustworthy superintelligence. Predictions for mathematical superintelligence in 2030 are discussed. Vlad and Tudor discuss their understanding of mathematics as reasoning, the core cognitive skills involved, and how these skills compare to the performance of frontier large language models.

00:08:31

The Beauty of Mathematics and AI's Role in Discovery

Vlad shares his journey into math through physics, highlighting the practical applications of physics inventions and the beauty of mathematics. The discussion touches on Eugene Wigner's essay and examples like differential geometry and number theory. The potential of AI in accelerating mathematical discovery is explored, differentiating between creative mathematicians and those who synthesize knowledge. AI's strength in information retrieval and application to unsolved problems is emphasized.

00:19:47

Understanding Lean: A Formal Verification Language and Its Impact

Lean is introduced as a programming language for formal verification. Its features, axioms (including the axiom of choice), and how it enables rigorous, step-by-step mathematical reasoning are explained. The transformation of mathematics from traditional methods to digital tools like Lean is discussed. The impact of Lean on collaboration, progress, and the potential elimination of traditional peer review is highlighted. A deeper dive into Lean's small, trusted kernel and its minimal axioms is provided. The concept of axioms, particularly the axiom of choice, and their role in building mathematics is clarified. A chess analogy is used to explain Lean's process. The use of Lean in mathematics education is discussed, with examples like the "natural number game" and "real analysis game," suggesting a shift from traditional chalkboards to computer labs.

00:37:06

Mathlib and Harmonic's Genesis: The Path to Superintelligence

Mathlib is introduced as a vast, open-source repository of formalized mathematical knowledge. It functions as a consolidated library of theorems and results, accessible and verifiable through Lean. The founding of Harmonic is tied to the maturation of Lean and GPT-4. The concept of mathematical superintelligence, combining formal verification with AI, is presented as their core mission.

00:40:06

Aristotle's Core Components and Refinements

The three core components of Aristotle are outlined: Monte Carlo tree search (similar to AlphaGo), an informal reasoning system for lemma guessing (acting as context management), and a specialized geometry module (AlphaGeometry). Vlad and Tudor discuss refinements to Aristotle since its IMO performance. The Monte Carlo tree search is clarified to involve high-level inference, and the informal reasoning system is described as a proposer of potentially incorrect steps.

00:47:42

Aristotle's Advanced Capabilities and the Boundaries of Reasoning

Beyond its core components, Aristotle's capabilities in auto-formalization (translating natural language to Lean) and theory building (creating new structures on the fly) are highlighted. The discussion explores the boundary between statements that can be mathematically proved and those that are philosophical or factual. The ultimate boundary of systems like Aristotle is defined as reasoning through any problem where valid steps of reasoning can be agreed upon, extending beyond mathematics to areas like software verification.

00:52:13

Training AI Models, Community, and the Future of Discovery

The conversation touches on training AI models, the potential bias from pre-trained models, model size, and the role of "taste" in AI development, balancing correctness with elegance and brevity. The decision to make Aristotle accessible to the community is discussed as a way to express "taste" through revealed preferences, allowing mathematicians to direct compute resources to problems they deem important. A philosophical debate on whether AI labs or empowered individuals will drive future discoveries is presented, with a preference for the latter. The challenge of evaluating AI-generated proofs for elegance is discussed, with brevity being a potential heuristic. Harmonic's belief in "The Bitter Lesson" is emphasized, suggesting that starting with pre-trained models is beneficial, but also the need to mix in reasoning systems with more entropy and complementary knowledge.

01:03:09

Interpretability, Trust, and the Vision for Aristotle

The discussion explores interpretability as a proxy for trustworthiness, Harmonic's focus on Lean for verifiable output, and the potential for AI to generate new abstractions and insights. The vision for Aristotle includes powering spacecraft, acting as a benevolent AI. The focus on formally verified output in Lean is presented as the solution to trustworthiness, rather than solely relying on interpretability.

01:06:41

Visualizing AI, Mathematical Structure, and Problem Difficulty

The visualization of large models as "shrink-wrapping reality" is discussed, with the expectation that mathematical models might be more interpretable internally due to their focused structure. The idea that AI models combine various mathematical techniques is explored, suggesting that understanding how models solve complex problems by integrating subfields could be more interpretable than analyzing weights. The current landscape of problem difficulty in AI-driven mathematics is sketched, from basic problems to unsolved conjectures and the IMO. The trend appears to be a smooth exponential, with potential for future breakthroughs.

01:08:47

IMO Performance, Formal Mathematics, and Software Verification

The consistent missing of Question 6 at the IMO by top AI labs is discussed, attributing it to its complexity and spatial reasoning requirements. The expectation is that such problems will eventually be solved. A significant phase transition to formal mathematics is identified, driven by AI's ability to auto-formalize complex papers. This shift moves humans from verifiers to "taste makers" in problem selection. The debate between formal and informal approaches in AI mathematics is declared settled, with formal methods being the clear future due to the need for verification of increasingly complex AI-generated proofs. The argument is extended to software, suggesting that as AI generates vast amounts of code, formal verification will become essential to ensure correctness and security, leading to a future of formally verifiable software. The initial adoption of formal verification will likely be in mission-critical software, accelerating the work of existing experts and gradually diffusing into broader software development. The compelling vision of totally verified, bug-free software is discussed, starting with critical systems and potentially extending to all software over time.

01:17:33

New Abstractions, Formal Reasoning, and AI's Role in Science

A question is raised about whether training AI within formal systems limits the emergence of new abstractions or "Einstein moments," and if current mathematical paradigms might prove insufficient in the future. Formal reasoning is presented as a detailed, computer-checkable version of informal reasoning. The minimal axioms of Lean are emphasized, suggesting no fundamental conflict between formal and informal approaches. Entropy and hallucinations are deemed crucial for AI systems, enabling exploration of novel concepts. The pursuit of hallucination-free LLMs is questioned, emphasizing the need for verification systems like Aristotle. Recent progress is reviewed, including gold performance at the IMO, solving previously unsolved problems, and the ongoing growth of Mathlib. The trend is towards formal reasoning becoming mainstream. The vision for mathematical superintelligence includes solving major problems and evolving beyond formal statements to potentially encompass intuitive physics and deducing all of physics from a single image. The discussion explores the potential for AI to accelerate scientific progress, leading to theoretical explanations for everything by 2030. It highlights the shift from intellectual bottlenecks to data limitations, requiring advanced experiments to validate theories.

01:29:33

AI Safety, Human-Centric Progress, and Conclusion

Concerns about the safety of advanced AI systems are raised, particularly regarding their potential power and the risks of cybersecurity incidents. The importance of constrained action spaces and learning from others' mistakes is emphasized. The speakers advocate for a future where humans remain central to progress, with AI accelerating advancements but humans retaining control. They stress the importance of making AI accessible and usable by people, not just a secret lab project.

Keywords

Q&A

• What is the core idea behind Harmonic's approach to mathematics?

  Harmonic views mathematics as fundamentally reasoning. They aim to build mathematical superintelligence by combining formal verification methods, like those used in the Lean programming language, with advanced AI techniques.

• How does the Aristotle AI system work?

  Aristotle uses a combination of Monte Carlo tree search (similar to AlphaGo) for exploring mathematical paths, a lemma guessing module for managing context, and a specialized geometry module. It also features auto-formalization capabilities.

• What is Lean and why is it important for Harmonic?

  Lean is a programming language and proof assistant that enables formal verification. Harmonic uses Lean to generate mathematically rigorous and automatically verifiable proofs, ensuring a high degree of trust and correctness in their AI's outputs.

• How does Harmonic's approach differ from other AI labs in mathematical competitions?

  While other labs might focus on informal reasoning, Harmonic emphasizes formal verification. This commitment to provable correctness, even if it requires more computational effort, is a key differentiator and contributes to their system's trustworthiness.

• What is Mathlib and its role in the future of mathematics?

  Mathlib is a vast, open-source repository of formalized mathematical knowledge written in Lean. It acts as a computationally certified "Wikipedia" for math, enabling easier verification and the building of new discoveries upon existing formalized knowledge.

• Can AI systems like Aristotle create new mathematical abstractions?

  While AI excels at applying existing knowledge and reasoning within formal systems, the emergence of truly novel abstractions is an ongoing area of research. Harmonic's approach focuses on rigorous verification, but the potential for AI to discover new mathematical structures is a key aspect of future development.

• What is the significance of "The Bitter Lesson" for Harmonic?

  Harmonic believes in "The Bitter Lesson," which suggests that general learning methods combined with large-scale computation are more effective long-term than human-designed heuristics. They leverage this by focusing on scalable AI training, often starting with pre-trained models.

• How does Harmonic ensure trustworthiness in its AI systems?

  Harmonic prioritizes trustworthiness by focusing on formally verified outputs using Lean. This means every proof generated by their system can be automatically checked, providing a high level of certainty and interpretability, unlike purely informal AI outputs.

• What is the future vision for mathematical superintelligence?

  Harmonic envisions a future where AI can solve increasingly complex mathematical problems, potentially leading to breakthroughs in science and technology. This includes formalizing vast amounts of mathematical knowledge and extending formal reasoning to other domains like software engineering.

• What role does entropy play in AI reasoning systems like Aristotle?

  Entropy, or randomness, is crucial for exploration in AI systems. It allows models to generate novel ideas and explore paths that might not be immediately obvious or formally correct, which is essential for discovering new mathematical concepts and solutions.

• What is the projected timeline for AI to provide theoretical explanations for all scientific phenomena?

  The speakers envision that by 2030, AI will have provided theoretical explanations for basically everything, shifting the bottleneck from intellectual discovery to data acquisition.

• What are the primary safety concerns regarding advanced AI systems?

  Initial dangers are expected to resemble cybersecurity incidents due to AI models making API calls and interacting with other systems, creating vulnerabilities and exploitation mechanisms.

• How can we ensure humans remain in control amidst rapid AI advancement?

  The speakers emphasize a human-centric approach, where AI accelerates progress but humans retain control and decision-making power. Making AI accessible and usable by people is crucial.

• What is the role of experimental data in future scientific progress?

  Once theoretical explanations are abundant, scientific progress will become data-limited. High-energy experiments will be crucial to differentiate between multiple valid theories, like those unifying quantum mechanics and general relativity.

Show Notes