01. – 06. Oktober 2023, Dagstuhl-Seminar 23401

Automated mathematics: integrating proofs, algorithms and data


Andrej Bauer (University of Ljubljana, SI)
Katja Bercic (University of Ljubljana, SI)
Florian Rabe (Universität Erlangen-Nürnberg, DE)
Nicolas Thiéry (University of Paris Sud – Orsay, FR)

Auskunft zu diesem Dagstuhl-Seminar erteilen

Jutka Gasiorowski zu administrativen Fragen

Michael Gerke zu wissenschaftlichen Fragen


Modern mathematical software and large databases of mathematical knowledge allow new approaches to solving mathematical problems, and support new kinds of mathematical exploration. The growing popularity of such approaches is increasingly straining the resources of the development teams. To make progress that will eventually result in a truly comprehensive and advanced computer mathematical assistant, the developers of individual software projects must start working together and tackle questions of interoperability, software engineering and knowledge management on a large scale.

This Dagstuhl Seminar plans to bring together system developers, library authors, and users from key branches of computer-supported mathematics: formalized mathematics, symbolic computation, and mathematical databases. The seminar aims to connect the communities, foster future collaboration across branches, and tackle problems that no branch can address alone. We shall address issues that are common to all areas of computer-supported mathematics: library management, dependencies and interoperability between software components, quality and correctness assurances, searching for information, and usability by end users.

Community building through interoperability. Participants will share their experiences and best practices, analyze common challenges, and work towards interoperability between existing systems. During the seminar, we will draft common terminology and information exchange protocols as a step towards serious integration of systems. We will rely on existing protocols, and will not depend on any particular system for automated mathematics. Doing so will allow computer supported mathematics to integrate more easily with other software systems.

Case studies. Participants from different communities will work on joint cases studies, for example by importing a library of mathematical knowledge from one system into another. The organizers will suggest challenges that require versatile expertise, for example formal verification of a mathematical dataset, incorporation of certain capabilities of a computer algebra system into a proof assistant, or enrichment of a mathematical dataset with new knowledge generated by a computer algebra system.

Impact. Advances in automated mathematics have a positive impact on research branches that rely on its methods and tools: formal verification of software and hardware systems uses proof assistants, applied mathematicians rely on computer algebra systems, and of course mathematicians themselves use automated mathematics in their research.

Motivation text license
  Creative Commons BY 4.0
  Andrej Bauer, Katja Berčič, Florian Rabe, and Nicolas Thiéry


  • Databases
  • Logic In Computer Science
  • Mathematical Software


  • Mathematical knowledge management
  • Mathematical software
  • Formalized mathematics
  • Computer algebra
  • Databases of mathematical structures


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.