https://www.dagstuhl.de/23401

October 1 – 6 , 2023, Dagstuhl Seminar 23401

Automated mathematics: integrating proofs, algorithms and data

Organizers

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)

For support, please contact

Jutka Gasiorowski for administrative matters

Michael Gerke for scientific matters

Motivation

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

Classification

  • Databases
  • Logic In Computer Science
  • Mathematical Software

Keywords

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

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.