Formal Verification, AI Hallucinations, and Mathematical Truth | Tudor Achim, Co-Founder, Harmonic

In this episode, Tudor Achim, Co-Founder and CEO of Harmonic, the AI lab behind Aristotle, a mathematical reasoning system that won gold at the International Math Olympiad, makes the case that AI hallucinations aren't the problem with today's models. The real problem is that nobody can verify whether a hallucination is right or wrong. Tudor explains why his team bakes formal, computer-checkable verification (using a language called Lean) directly into how Aristotle reasons, so instead of trusting an AI's word, you can mathematically prove it's correct.

Liam and Tudor go deep on what "truth" actually means in mathematics versus the real world, why Andrew Wiles's famous proof of Fermat's Last Theorem had a two-year hidden flaw, and why Tudor believes math is in the middle of its first fundamental shift in 4,000 years, moving from proofs written in English to proofs written in verifiable code. They also get into a spirited debate about the U.S. education system, what Harmonic actually looks for when hiring (hint: it's not the résumé), and why Tudor thinks AI will never be trusted to grade its own homework.

Key Topics Covered

What "truth" means in mathematics versus science, and why logical reasoning is really just a simple form of math

Why the proof of Fermat's Last Theorem had a hidden flaw for two years, even after being announced

Why hallucinations are actually necessary for AI reasoning, and what separates a good hallucination from a bad one

How Harmonic uses Lean and formal verification to make Aristotle's math proofs checkable step by step, like reviewing code

Why Tudor doesn't think any AI will ever be trusted to fully verify its own output

Why Harmonic gives away the Aristotle API for free right now, and where the business model is headed

The "phase transition" Tudor believes is happening in math for the first time in 4,000 years: from English proofs to machine-verified code

Why open-sourcing formal math matters more to Harmonic than keeping a competitive edge

Harmonic's five-year goal: contributing to solving a Millennium Prize Problem by 2028