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.
-
Jan Jakubův presented Learning-Guided Higher-Order Automated Reasoning for Isabelle/HOL (with Cezary Kaliszyk and Martin Suda) in the main track on September 22, on higher-order extensions of ENIGMA and Deepire evaluated on a large Isabelle/HOL corpus.