nice! i haven't gotten to TPIL yet but i suspect i might have to dive into it later β€” it seems more exhaustive than other resources, and doesn't assume math background RE:
Bluesky Social
Vikram Saraph (@vikramsaraph.com)
I wrote up proofs for the first set of exercises in Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean4/Propositions-an...
oh that's neat! RE:
Bluesky Social
Devon Govett (@devongovett.me)
btw, all the diagrams in this article are rendered using graphviz in a React Server Component to generate SVG at build time. Super convenient. [co...
barely a mention of atproto in this entire discussion (as well as the article) [The future is not self-hosted,...](
The future is not self-hosted, but self-sovereign | Hacker News
 )
tbh a lot of bluesky brand feels to me like "we added a hacky thing to solve what felt like a problem at a time and now we can't ever remove it although no other platform does this" RE:
Bluesky Social
alice (@alice.mosphere.at)
REPLY_NOTIF_DEPTH delenda est. literally no other platform does this. it's confusing and annoying and nobody knows about it exists the first place....
 View quoted note β†’
haven't watched fully yet but this explainer looks very promising [But how do AI images/videos ac...]( )
i worked on this proof for the entire week, and i finally got it working! i feel like i learned a lot about how to work with Lean. the proof is about showing that it's possible to construct a set of all functions from one set to another as long as you have some way to construct a set of all subsets [See https://leanprover.zulipch...](https://gist.github.com/gaearon/25a437a7b1773f4af94146af13d4fbd2 )
there's this liminal space of learning ability where you can already fix things with some luck but you don't fully understand why your fixes work. it's a funny feeling, like you have to rely on luck a bit and still can get royally lost but you're also not walking completely randomly. drunkard's fix
i think that’s pretty well thought out, especially the assurance that the internal repo main follows the public repo with force pushes. RE:
Bluesky Social
Paul Frazee (@pfrazee.com)
Hey devs! We're adopting some internal repos into our workflows at Bluesky, and I want to be clear about why and resolve any questions you have. T...
 View quoted note β†’
oh no, posts no longer have data-feed-context in the webapp. so it's harder to see where bad Discover posts are coming from :(
one thing that’s comforting about mathematics is that it doesn’t seem likely to fall apart with the passage of time (it did feel close to that a few times, but each time, it only came back richer and more magical β€” imo)