Dagstuhl Seminar 23401
Automated mathematics: integrating proofs, algorithms and data
( Oct 01 – Oct 06, 2023 )
Permalink
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 Paris-Saclay - Orsay, FR)
Contact
- Michael Gerke (for scientific matters)
- Jutka Gasiorowski (for administrative matters)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
- Upload (Use personal credentials as created in DOOR to log in)
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.

- Andrej Bauer (University of Ljubljana, SI) [dblp]
- Christoph Benzmüller (Universität Bamberg, DE) [dblp]
- Katja Bercic (University of Ljubljana, SI) [dblp]
- Alex Best (King's College - London, GB) [dblp]
- James Boyd (Wolfram Institute - Cambridge, US)
- Jacques Carette (McMaster University - Hamilton, CA) [dblp]
- Mario Carneiro (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Edgar Costa (MIT - Cambridge, US)
- James H. Davenport (University of Bath, GB) [dblp]
- Valeria de Paiva (Topos Institute - Berkeley, US) [dblp]
- Gilles Dowek (ENS - Gif-sur-Yvette, FR) [dblp]
- Catherine Dubois (ENSIIE - Evry, FR) [dblp]
- Stefania Dumbrava (ENSIIE - Paris, FR) [dblp]
- Madalina Erascu (West University of Timisoara, RO) [dblp]
- Jan Goedgebeur (KU Leuven, BE) [dblp]
- Kiran Gopinathan (National University of Singapore, SG) [dblp]
- Darij Grinberg (Drexel Univ. - Philadelphia, US) [dblp]
- Jyoti (Panjab University - Chandigarh, IN)
- Alexander Kasprzyk (University of Nottingham, GB) [dblp]
- Michael Kohlhase (Universität Erlangen-Nürnberg, DE) [dblp]
- Olexandr Konovalov (University of St Andrews, GB) [dblp]
- Filip Koprivec (University of Ljubljana, SI)
- Dimitri Leemans (UL - Brussels, BE) [dblp]
- Samuel Lelievre (University Paris-Saclay - Orsay, FR)
- Assia Mahboubi (INRIA - Nantes, FR) [dblp]
- Harshit J Motwani (Ghent University, BE) [dblp]
- Dennis Müller (Universität Erlangen-Nürnberg, DE) [dblp]
- Tobias Nipkow (TU München - Garching, DE) [dblp]
- Matej Petkovic (University of Ljubljana, SI) [dblp]
- Christian Pfrang (Bay. Min. für Digitales - München, DE)
- Florian Rabe (Universität Erlangen-Nürnberg, DE) [dblp]
- Talia Ringer (University of Illinois - Urbana-Champaign, US) [dblp]
- Claudio Sacerdoti Coen (University of Bologna, IT) [dblp]
- Kazuhiko Sakaguchi (INRIA - Nantes, FR) [dblp]
- Natarajan Shankar (SRI - Menlo Park, US) [dblp]
- Kathrin Stark (Heriot-Watt University - Edinburgh, GB) [dblp]
- Jure Taslak (University of Ljubljana, SI)
- Nicolas Thiéry (University Paris-Saclay - Orsay, FR) [dblp]
- Josef Urban (Czech Technical University - Prague, CZ) [dblp]
- Makarius Wenzel (Dr. Wenzel - Augsburg, DE) [dblp]
- Tom Kaspar Wiesing (Universität Erlangen-Nürnberg, DE)
Classification
- Databases
- Logic in Computer Science
- Mathematical Software
Keywords
- mathematical knowledge management
- mathematical software
- formalized mathematics
- computer algebra
- databases of mathematical structures