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.

Creative Commons BY 4.0

Andrej Bauer, Katja Bercic, Florian Rabe, and Nicolas Thiéry