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.
-
Jan Jakubův presented “Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL”, showcasing our progress on integrating machine learning into higher-order automated reasoning within the Isabelle/HOL ecosystem.
-
Keneni W. Tesema presented “Premise Selection for Higher-Order ATP Problems”, addressing the challenge of selecting relevant premises for higher-order automated theorem proving.