Aristotle, an AI theorem prover using Lean

Abstract: I'll describe the principles underlying the development of Aristotle, an AI theorem prover trained via reinforcement learning on Lean proofs. I'll give a demo of how this can be accessed and show some examples of projects making heavy use of this technology, in particular those using it for novel mathematical proofs and for library development.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026