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.

翻译：我们介绍一种基于机器学习的工具，用于Lean证明助手，该工具能够为用户正在证明的定理推荐相关前提。该工具的设计原则为：（1）与证明助手的紧密集成，（2）易于使用和安装，（3）轻量且高效的方法。为此，我们设计了一种自定义版本的随机森林模型，并以在线方式进行训练。该模型直接实现于Lean中，这一实现得益于Lean 4丰富且高效的元编程特性。随机森林模型基于从mathlib（Lean的数学库）中提取的数据进行训练。我们尝试了多种选项来生成训练特征与标签。用户可通过`suggest_premises`策略访问训练模型的建议，该策略可在交互式构造证明时于编辑器中调用。