Thanks for this nice post @ProfKinyon !
I'm currently trying to learn #lean and foolishly thought this was a good exercise to formalize!
In the end it was way beyond my current skills and I needed more time and way more AI help than I liked, but your proof works. 😅
https://tinyurl.com/4hzpyd6t
Thomas Kahle
@tomkalei@machteburch.social
Der radfahrende podcastende antifaschistische Matheprof und Papa aus Magdeburg. Math professor at OvGU Magdeburg posting in English and German. When I was young, we used to compile our own operating systems. 
Dauerkarte 
Searchable on tootfinder.ch
machteburch.social
Thomas Kahle
@tomkalei@machteburch.social
Der radfahrende podcastende antifaschistische Matheprof und Papa aus Magdeburg. Math professor at OvGU Magdeburg posting in English and German. When I was young, we used to compile our own operating systems. Dauerkarte Searchable on tootfinder.ch
machteburch.social
@tomkalei@machteburch.social
·
5d ago
2
1
1
Conversation (1)
Showing 0 of 1 cached locally.
Syncing comments from the remote thread. 1 more reply is still loading.
Loading comments...