Machine-Learned Premise Selection for Lean

TL;DR

This paper presents a lightweight, integrated machine learning tool for the Lean proof assistant that suggests relevant premises during theorem proving, utilizing a custom online-trained random forest model implemented in Lean 4.

Contribution

It introduces a novel, easy-to-use premise selection tool for Lean, leveraging a custom online random forest model integrated directly into the proof assistant.

Findings

Effective premise suggestions during interactive proofs

Fast and lightweight implementation in Lean 4

Trained on mathlib data for improved relevance

Abstract

We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are (1) tight integration with the proof assistant, (2) ease of use and installation, (3) a lightweight and fast approach. For this purpose, we designed a custom version of the random forest model, trained in an online fashion. It is implemented directly in Lean, which was possible thanks to the rich and efficient metaprogramming features of Lean 4. The random forest is trained on data extracted from mathlib -- Lean's mathematics library. We experiment with various options for producing training features and labels. The advice from a trained model is accessible to the user via the suggest_premises tactic which can be called in an editor while constructing a proof interactively.