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]