Machine-learned premise selection for Lean

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

Ramon Fernández Mir, Bartosz Piotrowski, Author name not available (Why is that?)

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
• A learning-based fact selector for Isabelle/HOL
• ATPboost: learning premise selection in binary setting with ATP feedback
• The Lean 4 theorem prover and programming language
• Online machine learning techniques for Coq: a comparison
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• ENIGMA: efficient learning-based inference guiding machine
• Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
• Hammering towards QED
• Random forests
• The Elements of Statistical Learning

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)