ML-based premise selection for Lean

Date: 10th March 2023
Time: 14:00 - 16:00
Location: IF 3.02

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

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.