Overview
This workshop is part of the 2026 CHAIR Research Themes program at Chalmers. The underlying theme, Cognition, Reasoning and AI in Collaboration, supports research activities spanning formalisation of mathematics, neuro-symbolic methods, reinforcement learning with feedback from provers, and cognitive aspects of reasoning AI.
The workshop aims to strengthen ties between Chalmers and related international research groups working in AI, reasoning, and formal mathematics.
Program
The schedule is tentative and may be updated. Slide links can be added to individual talks as they become available by replacing the placeholder link in the relevant program item.
Tuesday, 26 May
MV lunch/coffee room, second floor
Thierry Coquand, Devdatt Dubhashi, and Josef Urban — short talks. Room: Euler, Skeppsgränd 3.
Wednesday, 27 May
Martin Suda
Abstract
A neural clause-selection guidance approach in Vampire was recently shown to substantially improve the success rate of the prover's default strategy on TPTP. This talk studies the impact across ITP-derived benchmark sets and theorem proving strategies.Dennis Eriksson
Abstract
LLMs are fast, fluent, often useful, sometimes wrong, and always in need of supervision. This talk describes practical uses of LLMs in mathematical research, experimental mathematics, proof structuring, and writing.Dattabhasvant Ghadiyaram
Abstract
A Lean library using effective transversality for certified root finding in multivariate polynomial systems, including dyadic intervals, interval arithmetic, the Krawczyk method, custom syntax, and a tactic for certification.Thierry Coquand
Abstract
An experiment on autoformalising a proof of Gödel's second incompleteness theorem, using interaction with Claude and a system of primitive recursive arithmetic.Michael Rawson
Abstract
A talk loosely based on “When Vampire met Agda”, about connecting classical ATPs such as Vampire to constructive ITPs such as Agda.Thursday, 28 May
Jan Jakubův
Abstract
Higher-order extensions of ENIGMA and Deepire 2.0 are evaluated on a large Isabelle/HOL benchmark exported via Sledgehammer in several TPTP formats, showing complementary contributions from higher-order reasoning.Friday, 29 May
Room open for meetings, demos, discussions, and improvised talks.
Atle Hahn
Abstract
An update on the Naproche-ZF Autoformalization project with Adrian and Josef, including post-processing steps such as proof distillation, proof elaboration, and HTML rendering.Travel and administration
Chalmers strongly prefers to book travel tickets directly for invited participants. Attendees who plan to come are asked to send their preferred flight options as soon as possible to Andrea Brodén, with Moa Johansson copied.
Accommodation arrangements will be coordinated after the participant list is finalized.