Interactive and semi-automated theorem provers – Lean, Rocq, Isabelle/HOL, F*, Agda, Dafny, Verus, and others – have become indispensable tools for verifying safety-critical software and mechanizing mathematics. Formal proofs now appear in mainstream media, and breakthroughs in AI-assisted reasoning depend on these systems as their trusted formal foundation. Yet the theorem prover ecosystem remains deeply fragmented. Researchers and practitioners face incompatible foundations, logics, automation paradigms, and proof engineering philosophies. Expertise rarely transfers across systems, and hard-won lessons are repeatedly rediscovered in isolation.

At the same time, the rapid rise of AI-driven proof search and synthesis is reshaping what theorem provers can and should do. Large language models are being integrated as tactics, used for lemma discovery, and deployed for interactive proof guidance – but there is no shared understanding of how these capabilities should compose with traditional automation or with each other across systems.

This Dagstuhl Seminar aims to bring together researchers from across the theorem-proving landscape to critically examine the design decisions behind existing systems and to chart a course for the next generation of provers. Our goals are:

• To exchange concrete technical knowledge across communities: how automation is integrated with foundational proofs (Lean's grind, Isabelle's Sledgehammer, Rocq's SMTCoq), what works and what doesn't in rewriting vs. reduction-based proof styles, and how domain-specific frameworks (Iris, Veil, and others) extend base systems.
• To develop a blueprint for AI-native proof architectures – not as a replacement for human-guided reasoning, but as a composable layer that works alongside traditional tactics and automation.
• To identify grand challenge problems for the next twenty years of computer-assisted verification: ambitious goals that combine complex mathematics with software verification and go beyond the scope of existing benchmarks.
• To draft design principles for interoperating and composing theorem provers and AI-based verification tools, potentially in the form of new benchmarks in the spirit of the POPLMark Challenge.
• To address education and onboarding: how to lower the barriers for students, engineers, and industry practitioners who want to engage with mechanized proof, while equipping them to tell whether the theorems they prove actually say what they intend – a judgment that current tools do little to support.

This is a five-day seminar combining keynote talks on industrial verification experience, deep-dive tutorials by the developers of major proof assistants, research presentations, and breakout design sprints on future prover architectures and AI-proof ecosystems. A running hackathon-style problem will give participants a shared hands-on reference point throughout the week. We expect to produce a public, collaboratively drafted document containing a roadmap of moonshot challenges, a systematization of design principles for prover interoperability, and a consolidated index of educational resources – all hosted at a dedicated website. We also aim to seed multi-institution research collaborations and to outline a plan for a recurring school on AI-assisted formal verification and proof engineering.

The theorem-proving community is at an inflection point. The convergence of mature proof assistants, large-scale formalisation efforts, and AI-driven automation creates both an unprecedented opportunity and an urgent need to think across system boundaries. This seminar is designed to make that conversation happen.

Creative Commons BY 4.0

Sandrine Blazy, Jonathan Protzenko, Ilya Sergey, and Sebastian Ullrich

This seminar qualifies for Dagstuhl's LZI Junior Researchers program. Schloss Dagstuhl wishes to enable the participation of junior scientists with a specialisation fitting for this Dagstuhl Seminar, even if they are not on the radar of the organizers. Applications by outstanding junior scientists are possible until Friday, June 26, 2026.