3 ms·
Lean is the basis for my favorite puzzle game of the past five years: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk
by ahelwer 6y ago
Lean is the basis for my favorite puzzle game of the past five years: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...
It's like enemies & bosses are mathematical theorems you have to prove. Each time you slay one, you get it as a weapon you can use against further, more difficult bosses! The grand finale (Inequality World) is very memorable; such a feeling of accomplishment after I cracked it all. Then you zoom out and realize the math you've defeated reaches, like, fourth grade at most.
Lean revolutionized my understanding of math itself, which I wrote about here: https://ahelwer.ca/post/2020-04-05-lean-assignment/ https://ahelwer.ca/post/2020-04-05-lean-assignment/
- emrehan 6y agoHow many hours does it take to complete?
- ahelwer 6y agoI'd say 10 or so?
- cmehdy 6y agoThank you for sharing this, I'm having a lot of fun with it! I've been approaching proofs from a different angle, going through the book "How to prove it" and making a complicated setup to use an old applet recommended in the book (ProofDesigner, which requires old versions of Firefox to even load the applet). While that part helps with formal symbols, it's very rigid and aging compared to this fantastic resource and language.
- carapace 6y agoOh man that was fun! Totally nerd-sniped my day though. Got me to go back and re-watch Kevin Buzzard's talk at MS Research in re: Lean, "The Future of Mathematics?" https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721