Rendered at 18:16:26 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
fleshers 3 hours ago [-]
This is a solid intro.
I had no idea Lean was so Haskell-y and readable/practical in this way! For some reason I assumed it was just a clunky abstruse prover IDE type of thing, I guess I conflated it with older coq/Rocq and all the gigantic illegible ai math papers in recent news