ask me anything about Lean (theorem prover / programming language)!
caveat: i’ve only been learning it for a few months so i’m at a stage one could call “an inspired amateur”
the most difficult thing working in Lean for me is the mental adjustment about function evaluation.
in programming, there’s only a few things you can do with a function: refer to it or evaluate it. and you can’t influence evaluation
whereas in Lean, you can kind of reduce it yourself outside-in
agree seeing that post from official @npub1nfly...nul3 account was annoying. the fact that the “pin” feed exists SUCKS imo, it’s a hack not a feature
RE:
the part that doesn’t quite make sense to me is treating the skills necessary for overseeing today (“context engineering”, switching between AI workflows, knowing what diff models are good at) as some sort of a new core competency. i hope we’ll skip over that too, just like with “prompt engineering”
RE:
there’s something very satisfying about writing Lean proofs but i can’t quite explain it. it’s a different feeling from programming. with programming the feeling is that it comes alive. but in theorem proving, the feeling is that it “snaps together”. it doesn’t come alive but it’s the strongest bond
finally done with section 3.4, this was a bit rough! but i got a lot more comfortable with proofs that unwrap nested structures, `partial_functions` in particular was fun. looking forward to 3.5!
[Section 3.4 solutions by gaear...](
