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:
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
@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
@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
text/gemini
This content has been proxied by September (ba2dc).