Computer Tools for Pure Mathematics
Mini-Workshop, 27.-28.11.2014, Universität Freiburg
Topic: We will take a look at Mathematical Knowledge Management (MKM) and Proof Assistants. There will be a special focus on Homotopy Type Theory. We'll investigate the state of the art and where we can go from that.
- Thursday, 27.11.2014
- 12:30 - 13:00 obtain your nametag at SR 404, Eckerstr. 1
- 13:00 - 14:30 Michael Kohlhase
- 14:45 - 15:30 Konrad Voelkel
- 15:30 - 16:00 Coffee Break
- 16:00 - 17:30 Joachim Breitner
- 19:00 Dinner at Paradies
- Friday, 28.11.2014
- 10:00 - 11:00 Peter Arndt
- 11:00 - 11:30 Coffee Break
- 11:30 - 12:30 Peter Arndt
- 12:30 - 14:00 Lunch Break
- 14:00 - 15:00 Felix Wellen
- 15:00 - 15:30 Coffee Break
- 15:30 - 17:00 Hands-on session
- Prof. Dr. Michael Kohlhase, Computer Science, Jacobs University
Mathematical Knowledge Management and Information Retrieval: Transcending the One-Brain-Barrier
We present the emerging discipline of Mathematical Knowledge Management (MKM), which studies the possibility of computer-supporting and even automating the representation, cataloguing, retrieval, refactoring, plausibilization, change propagation and in some cases even application of mathematical knowledge.
We focus on theory graph technology here, which supports modular and thus space-efficient representations of mathematical knowledge and allows MKM systems to achieve a limited mathematical literacy that is necessary to complement the abilities of human mathematicians and thus to enhance their productivity.
- Dipl. Math. Konrad Voelkel, Mathematics, Universität Freiburg:
The Software Development Approach in Pure Mathematics
Taking into account that proofs are programs (made precise by type theory), and the move from documents to knowledge models (MKM), we look at some software tools that help pure mathematics and propose the development of new tools by semi-formalisation of mathematical content.
- Dipl.-Math. Dipl.-Inform. Joachim Breitner, Computer Science, KIT:
The proof assistant Isabelle
Isabelle is an interactive theorem prover. In other words: It is an editor for mathematical text that tell you where you might be wrong wrong (or just sloppy), but also where you are right.
We see Isabelle in action, proving a simple theorem. This will not teach you how to use Isabelle, but it will hopefully make you want to learn it. We also discuss its advantages and disadvantages over other theorem provers.
- Dipl. Math. Peter Arndt, Mathematics, Universität Regensburg:
(Homotopy) Type Theory
We will introduce the basic formalism of dependent type theory with identity types and its standard informal interpretations: logical (via the Curry-Howard isomorphism), set-theoretical/categorial and homotopy theoretical. Then we present the formal interpretation of type theory in model categories and discuss the univalence axiom and the usability of type theory as a tool and foundation for mathematics.
- Dipl. Math. Felix Wellen, Mathematics, KIT:
Verifying (Homotopy) Type Theory in Agda
We will look at some basic definitions and proofs in Agda with a focus on Homotopy Type Theory. Another aim is discussing some obstacles that occur while learning how to formalize Homotopy Type Theory in Agda.
Download the example code [updated 2014-12-09] which formalizes that the loop space of the 1-sphere are the integers. More recent code may be found on Felix' Homepage.
- Hands-on session: Bring your own device
Try out Isabelle, Agda, Coq, Univalent Foundations (or something else) and let experts help you overcome any difficulties in starting mechanized mathematics.
It is recommended that you enable
eduroamWLAN for your devices.
To try out Agda, we recommend that you install the agda and agda-mode packages of your Linux distribution before you arrive. This includes a "mode" for editing agda files in the text editor Emacs, which is highly recommended (for Agda, at least). Download and installation instructions for Agda may help you. Note that installing ghc and cabal from source shouldn't be necessary.
You might want to make yourself familiar with Emacs (if you not already are) by doing its inline tutorial. To do that, just start emacs and hit 'Ctrl-h' followed by 't'.
To try out Isabelle, follow the installation instructions for Isabelle. The most recent tutorial is “Programming and Proving in Isabelle/HOL”, which can be found at Isabelle’s Documentation page.
The large seminar room SR 404 is in the 4th floor of the main math building at Eckerstr. 1, which is close to the main train station. All talks will be in SR 404. For lunch, the Mensa "Institutsviertel" is very close but you can not pay by cash (stick to the locals!). There are other lunch options around the institute.
Registration is not stricly necessary, but highly appreciated, in order to have the right amount of coffee ready, and also if you want to participate in the dinner. Please write an informal email to the organiser before 15.11.2014.
There may be some limited funding available for students, please mention this in your email, if needed.
If you have any questions, don't hesitate to contact us.
To get an idea what the workshop is about (and far beyond), you can follow these links.
- Michael Kohlhase: Mathematical Knowledge Management (appeared in the June 2014 EMS Newsletter)
- The KWARC (Knowledge Adaptation and Reasoning for Content) group projects
- Thomas Hales: Developments in Formal Proofs (Seminaire Bourbaki, June 2014) and Thomas Hales: Mathematics in the Age of the Turing Machine (ArXiV, February 2013)
- The nLab (see also: what is the nLab, by Urs Schreiber), an open mathematics wiki.
- The Stacks Project, an open source book with some new features (most notably the tags system).
- The Homotopy Type Theory book (in particular the introduction) and its GIT repository (learn GIT), written in a massive collaboration.
- The Coq proof assistant and The Agda proof assistant, which both allow compiling formal proofs based on dependent type theory.
- Proof checker Isabelle and its proof archive
- The recent IHP special trimester on certified mathematics, also some lecture videos from the IHP.
Funding is generously provided by the Graduiertenkolleg 1821 "Cohomological Methods in Geometry".