Machine-learned premise selection for Lean

DOI10.1007/978-3-031-43513-3_10MaRDI QIDQ6541150zbMATH OpenFDO

Authors Bartosz Piotrowski, Ramon Fernández Mir

Publication date 17 May 2024

Copyright license Creative Commons Attribution 4.0 International

zbMATH Keywords

machine learningpremise selectionLean proof assistant

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A learning-based fact selector for Isabelle/HOL
• ATPboost: learning premise selection in binary setting with ATP feedback
• ENIGMA: efficient learning-based inference guiding machine
• Hammering towards QED
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• MizAR 40 for Mizar 40
• Online machine learning techniques for Coq: a comparison
• Overview and evaluation of premise selection techniques for large theory mathematics
• Premise selection for mathematics by corpus analysis and kernel methods
• Random forests
• The Elements of Statistical Learning
• The Lean 4 theorem prover and programming language

This page was built for publication: Machine-learned premise selection for Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6541150)