Extreme Value Distribution Project

This is a blueprint for a project which forms a part of the course MS-EV0029 Introduction to Formalized Mathematics in Lean at Aalto University, running from February to June, 2025. The goal is to formalize the Fisher-Tippett-Gnedenko theorem, classifying univariate extreme value distributions. Contributions are welcome by course participants!

WARNING: The blueprint is still work in progress! Contributions by the course participants to improve the blueprint and add details (which are helpful for formalization) are very welcome!