Presentation

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.