KRMT Project

This 5 ECTS project is a companion to the KRMT lecture which introduces basic concepts and practices in representing mathematical knowledge.

The project will be to formalize mathematical theories in a state of the art proof assistant.

Organization

The project will start around the 5th week of classes (so that the KRMT lecture can cover some prerequisite knowledge) with an admin meeting. Details will be announced.

Requirements: There are no formal requirements, but we strongly recommend that you either have taken the KRMT lecture or will take it in parallel. Furthermore, we assume that you have a high tolerance for mathematics (in particular mathematical proofs), logic and functional programming.

What Happens in the Project?

During the project you will solve formalization tasks about basic linear algebra in the proof assistant Isabelle. You are allowed to solve these tasks in teams.

At the end of the project there will be a presentation session where you have to present and/or answer questions about the tasks you worked on during the project. Details will be discussed in the admin meeting.

Communication

We will use our public KRMT Project matrix room for most of the data-to-day communication. Matrix is a communications platform that is supported by FAU. You can find instructions for joining Matrix at FAU here (only in German, unfortunately).