Vampire

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]

We are happy to present a collection of software tools developed by our team, spanning ML-guided theorem proving, algorithm configuration, proof visualization, and higher-order logic reasoning. See our Products page for downloads and source code.

• Deepire-2.0-HO — ML-based clause selection guidance for TPTP’s higher-order dialects in the Vampire prover, extending the Deepire learning framework to the higher-order setting.

• λENIGMA — ML-based clause selection guidance for TPTP’s higher-order dialects in the E prover, bringing ENIGMA’s learning-guided search to higher-order logic, including bug reports and fixes discovered during evaluation on Isabelle exports.

  [Read More]

Members of our Prague group participated in the Gothenburg CHAIR Workshop 2026 (May 26–29, 2026) at Chalmers University of Technology, Gothenburg, Sweden. The workshop brought together researchers working on AI-guided automated and interactive theorem proving.

We presented three talks covering our recent work:

• Martin Suda presented “Strong Within Benchmarks, Weak Across Them: Evaluating Neural Guidance in Vampire”, examining how learned guidance in the Vampire ATP system generalises across different problem benchmarks.

  [Read More]