The Future of Formal Mathematics is Here

Event Description

Simons Laufer Mathematical Sciences Institute presents...

In 2023, Tudor Achim co-founded Harmonic with Vlad Tenev to build the world's most advanced reasoning engine. Combining formal verification with informal reasoning, Harmonic's formal reasoning model, Aristotle, achieved gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver.

Achim is also the Co-Founder and former CTO of Helm.ai. He holds a B.S. in Computer Science from Carnegie Mellon University and was a PhD Candidate in Computer Science at Stanford University.

Register here: https://slmath.us10.list-manage.com/track/click?u=d58ee2e82c69809ff037f56b2&id=f07a675f6f&e=f1b6ba91e6

Date Start

Date End