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.

    Download slides of the talk

  • 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.

    Download the agda-mode emacs cheat sheet.

  • 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 eduroam WLAN 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.

Practical Information
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.

Further reading
To get an idea what the workshop is about (and far beyond), you can follow these links.

Funding is generously provided by the Graduiertenkolleg 1821 "Cohomological Methods in Geometry".