ABSTRACT

In 2025, Harmonic's Aristotle model achieved gold medal-level performance at the International Mathematical Olympiad by constructing formally verified proofs in the Lean proof assistant. Aristotle combines Monte Carlo tree search and reinforcement learning with interactive theorem proving to navigate vast search spaces and produce machine-checkable proofs of hard competition problems. Formal mathematics is a uniquely compelling domain for AI: it offers an unambiguous standard of correctness and a rich feedback signal for learning. This talk presents the architecture behind Aristotle, results on scaling these methods to increasingly difficult problems, and the implications of AI systems capable of research-level mathematical reasoning — including early applications in domains where guarantees of correctness are essential.

Tudor Achim is the CEO and Co-Founder of Harmonic, the AI lab building the world's most advanced reasoning engine. Under his leadership, Harmonic has pioneered the concept of Mathematical Superintelligence – the next generation of artificial intelligence that eliminates hallucinations by reasoning through mathematics as opposed to language prediction – and released the world's first consumer-facing MSI model, Aristotle. Aristotle recently achieved a gold medal-level performance at the 2025 International Mathematical Olympiad, demonstrating problem-solving capabilities that exceed human benchmarks.

Before founding Harmonic, Tudor co-founded and served as the CTO at Helm.ai, an autonomous driving software company. Tudor holds a B.S. in Computer Science from Carnegie Mellon University and was a Ph.D. Candidate in Computer Science at Stanford. He brings a rare combination of deep technical expertise and a vision to make mathematically grounded, provably accurate AI broadly available to individuals and institutions worldwide.