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.