Master Praktikum: Formalization in Lean (FiL)
Instructor: Xavier Généreux
2+2 hours per week
Prerequisites
The lecture on ITP is a prerequisite for this praktikum. This prerequisite is not strict but we will expect students to have seen and understood the material from the ITP course.
Overview
The Lean Theorem Prover is a functional programming language that double as an interactive theorem prover (ITP). In this Praktikum, we will explore how to use the Lean Theorem Prover to formalize non-trivial theories. Your objective will be to formalise some fact in mathematics or computer science.
Organization
The semester will be split into two parts:
Part 1 : Background
In the first part of this Praktikum, we will review the material needed for your formalization projects. This will take the form of weekly lectures where we will make an overview of the different subjects possible for the projects and introduce the technicalities of each one. These will cover different topics in mathematics and also computer science. During this time, students will be required to complete homework. These should be handed in before the start of the projects.
Homework
To access the homework follow these steps (see Lean projects for more info):
- Go the the directory where you would like this package to live.
- Run
git clone https://github.com/genereuxx/formalization_in_lean_2024.git
. - Run
cd formalization_in_lean_2024
. - Run
lake exe cache get
. (This takes a little while) - Run
code .
to open the project. If you open it from a menu, you need to open theformalization_in_lean_2024
folder.
Deadline
The deadline for the homework is 06.12.2024 at 23:59.
To submit the homework, please do a private Github repository and invite me before the deadline.
Part 2 : Projects
In the second part, the project phase will commence, with students working in teams of 2 or 3. The main goal of the projects should be to formalise a series of mathematical results, the correctness of an algorithm or properties for some semantic.
Evaluation
Each team will also be tasked with delivering a presentation on their project. Evaluation will be based on the complexity of the theory, the technical difficulty of its formalisation, the readability of the code and the documentation. Student are also expected to produce a text with the following content:
- Review of the target theory and motivation
- Highlight and main challenges of the formalisation and their solutions
- Design decisions taken during the development and their motivation
- Shortcomings of the project and possible futur work
The text should be between 7.000 and 14.000 characters. (~4 to 7 pages)
Topics
Here you can find some general directions that you can take for the projects. If you choose to formalize a theory that follows a textbook, you should formalize at least some of the exercises and their solutions.
Computer science:
- extended WHILE language with static arrays or other features;
- functional data structures (e.g., balanced trees);
- functional algorithms (e.g., bubble sort, merge sort, Tarjan’s algorithm);
- type systems (e.g., Benjamin Pierce’s __Types and Programming Languages__);
- security properties (e.g., Volpano–Smith-style noninterference analysis);
- theory of first-order terms, including matching, term rewriting;
- automata theory;
- normalization of context-free grammars or regular expressions;
- chapters of concrete semantics;
- soundness and completeness of proof systems (e.g., Genzen’s sequent, calculus, natural deduction, tableaux);
- separation logic;
- verified program using Hoare logic;
- model a language like SQL and prove facts about it;
Mathematics:
Any kind of mathematical project is possible. They must however be significantly different from existing lean formalisations.
- Port formalized problems from another language to Lean;
- Formalise a chapter of a textbook (e.g. Understanding Analysis);
Further information
You have, at the latest, until December 20th to lock in your project’s topic. Please write on the “Projects” thread on the course’s Zulip with your team’s members and a summary of your project. Example:
-
@Name1 @Name2 and myself will be working on Formally real fields, with the goal of proving formally that such fields are orderable.
We intend to prove it by applying Zorn’s lemma, to show that a formally real field contains a maximal positive cone, and that the latter defines a total positive cone in the sense of
mathlib
. And then it is proved inmathlib
that such a cone defines an ordering.
During the middle of the project phase, there will be a mandatory meeting with me to review your progress in the projects. (16, 27 or 30th of January.) Otherwise, you will have the possibility to meet me weekly during class hours to ask questions. (See Schedule below.)
The projects are open ended, you can push them as far as you want. Even with mathematical theorems, there are often optimisations, related facts or generalization available as an open direction.
Deadline
The deadline for the project is Sunday March 2rd 23:59. Please send me your report on Zulip or by email. Only one person per team needs to submit the report. Please mention all your team member’s when you submit.
The code review will take place on Monday March 3rd from 13:00 to 16:00 in Oettingenstr. 67 - 131.
Please consult the Room change and final presentation
thread on Zulip to reserve your time slot.
Schedule (Updated for the project phase)
Availabilities
By appointment : Monday 16:00 - 18:00
In person: Thursday 13:00 - 15:00 c.t. Oettingenstr. 67 - L109, Floor Plan
Exceptions
As discussed in class, there are some exceptions :
- The week of December 8th : No availabilities this week.
- The week of December 15th : By appointment; by zoom only.
- The week of January 19th : No availabilities this week.
- The week of January 26th : Mandatory progress update
- Thursday February 13th : Room change : Oettingenstr. 67 - 165
During these weeks, you can of course send me your questions on Zulip or by mail. To make up for the two missed weeks, I will offer the normal availabilities on the weeks of February 9 and 16.
Chat
There is a Zulip chat room associated with the lecture where you can ask organizational and content-related questions. Please use it if possible, instead of sending me emails, so that your fellow students can also benefit from the answers.
Zulip-Stream: Formalization in Lean chat
Material
Getting started
Main ressources
Search engines
Other
Artikelaktionen