KRMT Project

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

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

Organization

The project will start in the 5th week of classes (so that the KRMT course 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 course or will take it in parallel. Furthermore, we assume that you have a high tolerance for mathematics, logic and functional programming.

What happens in the project?

We will start with a warm-up problem, in which you will formalize some basic proofs in the area of naive set theory which is introduced in (the current iteration of) the KRMT lecture, to be solved in the proof assistant [Isabelle]{https://isabelle.in.tum.de/}.

After that warm-up problem, the problems contain formalization tasks in the area of real linear algebra, again to be solved in Isabelle.

All problems can be solved in teams.

Furthermore, at the end of the project you will have to give a presentation of your formalizations. The 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).