Mar, 2023
基于机器学习的精简前提选择
Machine-Learned Premise Selection for Lean
Bartosz Piotrowski, Ramon Fernández Mir, Edward Ayers
TL;DR我们设计了一个基于机器学习的工具,用于 Lean 证明助手,可以为用户正在证明的定理提供建议,它是通过在线训练自定义版本的随机森林模型,并利用 Lean 4 的元编程特性直接实现,可以通过 suggest_premises 策略在编辑器中与用户进行交互式证明