Subscribe to Events

In 2025, Harmonic, along with three other companies, achieved a gold medal-level performance at the IMO with AI systems, a feat that could only have been described as science fiction not many years ago. In this talk, I will present Aristotle, our reinforcement learning system that achieved this feat, discussing both its Monte Carlo tree search-based Lean proof search, and the frameworks we used to augment its capabilities - test-time training, and lemma generation. I will then highlight some work done by newer versions of Aristotle, autonomously solving problems without human input, and assisting mathematicians with large-scale formalizations.