Conférences  >  Mathématiques  >  Démonstration automatique de théorèmes

Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH

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.

The International Centre for Mathematical Sciences (ICMS)

Validated numerics, rooted in Moore’s interval analysis, uses the arithmetic of real intervals to rigorously bound nonlinear functions and control floating-point errors in computations. These methods extend naturally to higher-dimensional and function spaces, forming the basis of rigorous numerical functional analysis. Combined with set-oriented techniques, validated numerics has enabled computer-assisted proofs to address a variety of problems in dynamical systems. Recent advances in computing, and wider availability of platforms that provide support, have led to a resurgence of research activity in the field of validated numerics (and application to computer-assisted proofs).

Isaac Newton Institute for Mathematical Sciences, Cambridge