Isabelle

Our team gave three talks at CICM 2026 (Conference on Intelligent Computer Mathematics), held in Ljubljana on September 21–25:

• Jan Jakubův gave an invited lecture A Decade of ATP Tuning: Machine Learning, Strategy Invention, and AI in the Future at the AI4Math workshop on September 21 (slides).

• Jeremy Lindsay presented Optimising Metamath Proofs for Human Working Memory (with Cezary Kaliszyk and Christine Rizkallah) in the main track on September 22, on reordering proof steps to reduce the working-memory demand on human readers.

  [Read More]

Two members of our team gave talks at AITP 2026 (Conference on Artificial Intelligence and Theorem Proving) on September 1:

• Jan Jakubův presented Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL, on higher-order extensions of ENIGMA and Deepire evaluated on a large Isabelle/HOL corpus.

• Keneni W. Tesema presented Premise Selection for Higher-Order ATP Problems, on selecting relevant premises for higher-order automated theorem proving.

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]

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]