Deep Exploratory Engine for Precise Expert Reasoning

The project is concerned with developing machine learning guidance for modern state-of-the-art automatic theorem provers (ATPs) capable of generating correct proofs. In particular, it focuses on AI guidance for higher-order and dependently typed calculi, which are essential for directly addressing problems in the formalization of mathematics, as well as guidance for the Prover9 system, which plays a crucial role in the AIM project by Kinyon and Veroff. The approach combines neural and symbolic learning methods: deep learning for proof guidance is complemented by the hints method, which is critical in handling very large proofs of open conjectures.

Goals

To achieve the overall goal of powerful automated reasoning for mathematics, the project pursues the following four objectives:

  1. Developing effective AI-based guidance for higher-order automated reasoning systems that can prove large numbers of goals in formalized mathematics libraries.

  2. Designing proof advice and efficient automation for dependently typed proof foundations.

  3. Integrating strong guided automated theorem provers into modern state-of-the-art proof assistants, including their hammer systems, and optimizing them for large proof libraries.

  4. Advancing towards an autonomous reasoning system able to tackle open mathematical problems, using learning techniques such as conjecturing, reinforcement, and inspiration from existing proofs.

Funding

This project is funded by the Renaissance Philanthropy grant project DEEPER.

Partnership

The project is an international cooperation between

uniting complementary expertise to develop AI-guided automated reasoning systems.

UoM CTU

πŸ“œ New Publications

Recent papers from the Deeper4AI team accepted for publication

 Posted on June 30, 2026  |  Deeper4AI @ Melbourne & Prague

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]
Publications  TheoremProving  Autoformalization  MachineLearning  Isabelle  Vampire  EProver 

πŸ› οΈ New Products

Software tools and prototypes from the Deeper4AI team

 Posted on June 30, 2026  |  Deeper4AI @ Melbourne & Prague

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]
Products  TheoremProving  MachineLearning  Vampire  EProver  Visualization 

πŸ›οΈ CHAIR Workshop 2026

Gothenburg CHAIR Workshop on AI and Automated Reasoning, Chalmers University of Technology

 Posted on May 26, 2026  |  Deeper4AI @ Prague

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]
Workshop  TheoremProving  MachineLearning  Vampire  EProver  Isabelle 

πŸ“’ Postdoctoral position [CLOSED]

AI-Guided Theorem Proving in Higher-Order Logic and Algebraic Domains

 Posted on August 15, 2025  |  Deeper4AI @ Prague

We are excited to announce one fully funded postdoctoral research position as part of our newly accepted project on AI-driven automated reasoning for higher-order logic and algebraic theories. The project builds on recent breakthroughs such as Enigma, Deepire, and Monte Carlo proof search, and aims to develop autonomous reasoning systems that combine symbolic and statistical guidance, applied to open research-level problems in algebraic domains (e.g., loop theory, AIM Conjecture) and large-theory interactive theorem proving.

[Read More]
Postdoc  TheoremProving  NeuroSymbolic  FormalMethods