We are happy to announce a series of new papers from our team, all accepted for publication. The work spans two intertwined themes: large-scale LLM-assisted autoformalization of mathematical textbooks, and machine learning guidance for higher-order automated theorem proving. See our Publications page for details.
-
Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL. We present higher-order extensions of ENIGMA and Deepire — the two prominent learning-guided reasoning systems for the E and Vampire provers — and evaluate them on a large Isabelle/HOL corpus emulating Sledgehammer, observing consistent improvement across the board.
[Read More]