Functional analysis in Lean

Lean is an interactive proof assistant, meaning a program in which it is which it is possible to prove mathematical theorems. Proof wizards have been recently used to verify a technical lemma in the field of algebraic geometry (the Liquid Tensor Experiment initiated by Peter Scholze). In analysis, the mathematical library of Lean is not very powerful yet and the goal of this project is to make a contribution to functional analysis.

Recommended are basic knowledge in the areas of analysis and linear algebra. Basic knowledge in functional analysis and programming experience would be advantageous. The duration of the work within the research group should be at least four weeks. In addition, a written elaboration and a final presentation in the seminar is expected.