the thing that’s exciting to me about Lean is that it’s able to capture things in the mathematical sense (obviously because that’s its purpose). i’m so used to dealing with floats or int or JS Numbers, it’s hard to imagine reals and their properties actually being captured. same with props, sets
imo this track is playing too safe to be great but the the hook is incredibly addictive, wonderful earworm at 2:38. i love the internal rhyme and the alliteration in that line [www.youtube.com/watch?v=ZERd...]( )
[SASAMI - Just Be Friends (Lyri...]( )
i’m having an unreasonable amount of fun learning lean and i’m worried re what this means for my future job safety. both in the sense of formalized theorem proving being probably the most llm-friendly part of mathematics and in the sense of i doubt there is any money in it despite being v addictive
