Machine-learned premise selection for Lean

DOI10.1007/978-3-031-43513-3_10MaRDI QIDQ6541150FDOQ6541150

Authors: Bartosz Piotrowski, Ramon Fernández Mir 

Publication date: 17 May 2024

zbMATH Keywords

machine learningpremise selectionLean proof assistant

Mathematics Subject Classification ID

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

Cites Work

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

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)