Lean is the basis for my favorite puzzle game of the past five years: 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/