Title: ML-based premise selection for Lean
Speaker: Ramon Fernández Mir
Abstract:

In this talk, I will introduce a machine-learning-based tool for the Lean theorem prover that suggests relevant premises to a user interactively constructing a proof. The tool, entirely written in Lean 4, is designed to be highly user-friendly, customizable, and efficient. It is based on a version of random forest, trained on data extracted from mathlib — Lean’s mathematics library. I will discuss one of the main challenges, which was producing useful training features and labels. Finally, I will give a short demo and talk about some interesting related work.