A great success of 20th-century mathematical logic has been the development of proof systems for putting mathematics on a firm basis, clarifying foundational options and their interaction. However, a pivotal question arises: Can these proof systems extend beyond foundational theory to offer practical benefits in mathematics and computer science? In particular, do proof systems facilitate proofs of new results, better or automated proofs of established results, or computer formalization of specific subjects in mathematics and computer science?

A partial positive answer is given by synthetic frameworks for specific subjects in mathematics and computer science, the most well-known of which presumably is Euclid's synthetic geometry. Unlike Descartes' coordinate-centered analytic geometry, where points and lines are encoded as (pairs or sets of) numbers, the synthetic account puts points and lines as primitive concepts governed only by axioms. As such, synthetic geometry provides custom-tailored foundations to geometry. Synthetic frameworks have proved to be pivotal tools at the interface of mathematics and computer science, especially in enabling concise formalizations. Way beyond Euclid's synthetic geometry, noteworthy present achievements include homotopy type theory, synthetic computability theory, synthetic differential geometry and synthetic algebraic geometry.

Further affirmative answers emerge from logic-driven computational algebra and geometry, and the proof assistants centered on coherent logic. These topics are interconnected through shared logical methodologies such as sheaf models, syntactic translations, novel developments in realizability theory, and strong negation for constructive reasoning with negative information. In particular, enhancing the current logical models of computation to incorporate computational side-effects from programming languages brings in new models with interesting properties.

This Dagstuhl Seminar seeks to extend and deepen the convergence across disciplinary boundaries by fostering exchange and collaboration among the relevant experts and practitioners, uniting expertise in proof theory with proof complexity, categorical semantics, constructive mathematics, proof mining, program extraction, and automated theorem proving. By bridging these domains, we seek to empower the next generation of researchers to frame and connect their work within this converging landscape, ultimately advancing the computational applications of proof systems in both theoretical and practical contexts.

Creative Commons BY 4.0

Ingo Blechschmidt, Liron Cohen, Thierry Coquand, and Peter M. Schuster