i love that you can cmd+click into some Lean builtin thing and it'll have that vibe... idk. like, casually fundamental. here's one of the most important structures in the universe, here's what we had to do to make it fast and tolerable to work with https://morel.us-east.host.bsky.network/xrpc/com.atproto.sync.getBlob?did=did:plc:fpruhuo22xkm5o7ttr2ktxdo&cid=bafkreicimbasim35mnzbca5vpub2ilkloavnmxexnvj6d2ausyzbalq4fa

this is great actually and is pretty much how i'm using claude RE:

Bluesky Social

The Verge (@theverge.com)

Google would like you to study with Gemini instead of cheat with it https://buff.ly/LmmBimS

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

generalize_proofs is probably my new favorite Lean tactic

agree seeing that post from official @Bluesky account was annoying. the fact that the “pin” feed exists SUCKS imo, it’s a hack not a feature RE:

Bluesky Social

Bluesky

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:

Bluesky Social

Kuba Suder 🇵🇱🇺🇦 (@mackuba.eu)

Interesting overview of how software development jobs (& recruitment, and education) are changing and will be changing in near future because of AI...

View quoted note →

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

new type of annoying pattern is people filing nonsensical AI-generated issues and other people sending nonsensical PRs trying to fix those issues

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...](

GitHub

Section 3.4 solutions by gaearon · Pull Request #7 · gaearon/analysis-solutions

)