Alex Best - Aristotle, an AI theorem prover using Lean

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic for the talk

[Ryan McCorvie]

Thanks for the really interesting talk. It's been really exciting to follow how quickly solutions to Erdos problems have been formalized with Aristotle.

Has Harmonic published white papers or technical document with more details about how it uses RL and search? I am aware of this one related to the IMO: https://arxiv.org/html/2510.01346v1

[Alex J. Best]

That's the main one right now, we have a few other details on some of the components you may find interesting over at https://harmonic.fun/news but only that one whitepaper.