Dagstuhl Seminar 18341
Formalization of Mathematics in Type Theory
( Aug 19 – Aug 24, 2018 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/18341
Organizers
- Andrej Bauer (University of Ljubljana, SI)
- Martín H. Escardó (University of Birmingham, GB)
- Peter L. Lumsdaine (University of Stockholm, SE)
- Assia Mahboubi (INRIA - Nantes, FR)
Contact
- Shida Kunz (for scientific matters)
- Annette Beyer (for administrative matters)
Formalized mathematics is mathematical knowledge (definitions, theorems, and proofs) represented in digital form suitable for computer processing. A formalized theorem has a very high correctness guarantee, as its proof is mechanically checked in complete detail. The formalized mathematics community has been growing steadily, with several research groups having recently completed major n goals, each using slightly different approaches and software tools. The complexity and the structure of these efforts resemble those of large software projects. Indeed, the recent successes in formalization can in part be attributed to adoption of software engineering practices and tools for software development.
But formalized mathematics is much more than proof-checking: it can help with verification of large scale computations, discovery of new constructions and proofs, organization of mathematical knowledge, and cooperation between mathematicians that surpasses current practice. The central goal of this seminar is to identify the theoretical advances and practical improvements needed in the area of formalized mathematics, in order to make it a mature technology, truly useful to a larger community of students and researchers in mathematics.
This Dagstuhl Seminar will be a place for sharing ideas, tools, techniques, and the needs of those who formalize mathematics, or want to learn about it. It will bring together the developers of proof assistants, the experts on formalization, and the mathematicians interested in formalization. We will focus not only on bare formalization in proof assistants, but also on tools for mathematical exploration, such as symbolic computation, use of heuristics, and machine learning, as well as interfaces between them and the proof assistants.
Our program will offer tutorials and a limited number of talks. We will leave ample time for work and discussions in smaller groups. The participants will informally report their ideas and findings in a spur-of-the-moment fashion.
Creative Commons BY 3.0 DE
Andrej Bauer, Martín H. Escardó, Peter L. Lumsdaine, and Assia Mahboubi
We and all the participants were delighted to benefit from Dagstuhl's inspiring environment.
Proof assistants are receiving increased attention from users with a background in mathematics, as opposed to their traditional users from theoretical computer science/logic/program verification, and this was the major focus of the meeting. This is true in particular of proof assistants based on dependent types, probably due in part to the advent of homotopy type theory, developed in the proof assistants Coq, Agda and Lean.
The audience of the seminar was thus rather unusual in composition, and featured several experienced researchers used to attending seminars at the Mathematisches Forschungsinstitut Oberwolfach, and visiting Schloss Dagstuhl for the first time. In order to foster discussion and fuse collaborations, we adopted a different format from the standard string of slide-based talks: talks in the morning, so that people get to know the work of each other, and working in groups in the afternoon. At the end of each day, before dinner, each group presented a summary of the outcomes of their meetings to all participants, which allowed inter-group discussion and collaboration. This had been tried before by some of the organizers, in the course of Dagstuhl seminar 16112, and worked just as well in our case.
Working group topics were proposed by the audience on the first day, by giving short presentations of a few minutes and writing topics in the board. Some were quite specialized and homogeneous (e.g. the cubical type theory group), and allowed people to have a focussed collaborative brainstorming on a specific open problem of the field. Some were more open-ended, and allowed people to confront various approaches to the same issue/concept in different systems (different proof assistants, computer algebra systems, etc.).
Some people did applied work, such as trying to compute the so-called Brunerie number from an existing proof in homotopy type theory, in order to identity and fix inefficiency problems in proofs assistants based on cubical type theory. Some people used their spare time to solve the ``Dagstuhl dinner'' problem. Details of the topics discussed are in the reports produced by each group.
This was a rather productive meeting, and people from different scientific backgrounds not only met but talked together effectively, solving and identifying problems to work on collaboratively in future.
Andrej Bauer, Martín H. Escardó, Peter L. Lumsdaine, and Assia Mahboubi
- Benedikt Ahrens (University of Birmingham, GB) [dblp]
- Carlo Angiuli (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Andrej Bauer (University of Ljubljana, SI) [dblp]
- Sophie Bernard (INRIA Sophia Antipolis, FR) [dblp]
- Yves Bertot (INRIA Sophia Antipolis, FR) [dblp]
- Auke Booij (University of Birmingham, GB) [dblp]
- Guillaume Brunerie (University of Stockholm, SE) [dblp]
- Jacques Carette (McMaster University - Hamilton, CA) [dblp]
- Mario Carneiro (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Cyril Cohen (INRIA Sophia Antipolis, FR) [dblp]
- Manuel Eberl (TU München, DE) [dblp]
- Martín H. Escardó (University of Birmingham, GB) [dblp]
- Diane Gallois-Wong (Laboratoire de Recherche en Informatique - Orsay, FR) [dblp]
- Gaëtan Gilbert (INRIA - Nantes, FR) [dblp]
- Georges Gonthier (INRIA Saclay - Île-de-France, FR) [dblp]
- Daniel R. Grayson (Urbana, US) [dblp]
- Philipp Haselwarter (University of Ljubljana, SI) [dblp]
- Florent Hivert (Laboratoire de Recherche en Informatique - Orsay, FR) [dblp]
- Johannes Hölzl (Free University Amsterdam, NL) [dblp]
- Kuen-Bang (Favonia) Hou (University of Minnesota - Minneapolis, US) [dblp]
- Simon Huber (University of Göteborg, SE) [dblp]
- Fabian Immler (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Nicolai Kraus (University of Nottingham, GB) [dblp]
- Dan Licata (Wesleyan University - Middletown, US) [dblp]
- Peter L. Lumsdaine (University of Stockholm, SE) [dblp]
- Assia Mahboubi (INRIA - Nantes, FR) [dblp]
- Maria Emilia Maietti (University of Padova, IT) [dblp]
- Scott Morrison (Australian National University - Canberra, AU) [dblp]
- Anders Mörtberg (Chalmers University of Technology - Göteborg, SE) [dblp]
- Russell O'Connor (Blockstream - Montreal, CA) [dblp]
- Ian Orton (University of Cambridge, GB) [dblp]
- Anja Petkovic Komel (University of Ljubljana, SI)
- Claudio Sacerdoti Coen (University of Bologna, IT) [dblp]
- Bas Spitters (Aarhus University, DK) [dblp]
- Jonathan Sterling (Carnegie Mellon University - Pittsburgh, US) [dblp]
- Neil Strickland (University of Sheffield, GB)
- Michael Trott (Wolfram Research - Champaign, US) [dblp]
- Hoang Le Truong (Universität des Saarlandes, DE) [dblp]
- Josef Urban (Czech Technical University - Prague, CZ) [dblp]
- Floris van Doorn (University of Pittsburgh, US) [dblp]
- Makarius Wenzel (Augsburg, DE) [dblp]
- Bohua Zhan (Chinese Academy of Sciences - Beijing, CN) [dblp]
Classification
- semantics / formal methods
- verification / logic
Keywords
- formalized mathematics
- type theory
- proof assistant
- formal methods
