Toot

Written by Andrej Bauer on 2024-11-28 at 16:51

I am teaching a course on formalized mathematics in Lean (https://www.andrej.com/zapiski/MAT-FORMATH-2024/book/). I let the students pick their own formalization projects, and this is what they've come up with:

1. The tripos-to-topos construction

2. Elementary toposes

3. Kripke models of modal logic

4. (Localic) Stone duality

5. Master theorem https://en.wikipedia.org/wiki/Master_theorem_(analysis_of_algorithms)

6. Wedderburn–Artin theorem https://en.wikipedia.org/wiki/Wedderburn–Artin_theorem

7. Blossoms https://en.wikipedia.org/wiki/Blossom_(functional)

8. Relative monads

9. Nyquist-Shannon sampling theorem https://en.wikipedia.org/wiki/Nyquist–Shannon_sampling_theorem

10. Steiner systems https://en.wikipedia.org/wiki/Steiner_system

11. Pólya enumeration theorem https://en.wikipedia.org/wiki/Pólya_enumeration_theorem

I wonder whether I am a pessimist or they are all optimists. Anyhow, it's going to be fun to watch their blueprints turn green.

P.S. To show the students how it's done, I am doing my own project on partial combinatory algebras https://github.com/andrejbauer/partial-combinatory-algebras It's a race!

=> More informations about this toot | View the thread | More toots from andrejbauer@mathstodon.xyz

Mentions

Tags