Prof. Cezary Kaliszyk gave an invited talk at SCML-2026, the conference on Symbolic Computation and Machine Learning, held July 6β8, 2026 in Hagenberg, Austria.
His talk, “Formalization and Automated Reasoning in the Age of LLMs”, was presented on Monday, July 6, and discussed how large language models are reshaping formalization and automated reasoning. The slides are available here.
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]