Ancestors

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 | More toots from andrejbauer@mathstodon.xyz

Descendants

Written by Wen on 2024-11-28 at 17:40

@andrejbauer Always interesting. Of course an expectation (from a mathematician) is that several of these will be unsolvable, and some others might throw useful light on the problems. But then young 'inexperienced' mathematicians often take the world by surprise. And that is how it should be.

=> More informations about this toot | More toots from Wen@mastodon.scot

Written by Andrej Bauer on 2024-11-28 at 21:38

@Wen I imposed a condition that they should formalize mathematics that they know well already.

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

Written by Jacques Carette on 2024-11-29 at 01:11

@andrejbauer That's a mighty impressive list!

=> More informations about this toot | More toots from JacquesC2@types.pl

Written by Andrej Bauer on 2024-11-29 at 07:38

@JacquesC2 Yes, we shall see. This is the list after I vetoed proposals that amounted to PhDs and research projects...

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

Written by Gina Peter Banyard on 2024-11-29 at 09:06

@andrejbauer what academic level is this?

Having done @xenaproject course at Imperial College back in Spring 2022 as a 3rd year Mathematics student, those feel ambitious?

How long are the projects meant to last?

=> More informations about this toot | More toots from Girgias@phpc.social

Written by Counting Is Hard on 2024-11-29 at 16:12

@andrejbauer A person's reach should exceed their grasp or what's a heaven for

(https://www.poetryfoundation.org/poems/43745/andrea-del-sarto)

=> More informations about this toot | More toots from counting_is_hard@mathstodon.xyz