having a bunch of fun with #lean4

they got me to do maths with it and have fun, and now i somewhat want to learn more mathematics. talk to your children about theorem provers before some dependent types dealer gets to them first :p