danabramov.bsky.social
@danabramov.bsky.social
i wonder what it would look like if blocklists were kind of voluntary. like “yeah i talk about ai” but you add yourself to it, rather than get added by someone. like a badge you wear. and you can choose to block out all people wearing some badge if you want
July 10, 2025 at 2:28 AM
for some reason this is really funny to me
July 9, 2025 at 2:21 AM
learned a lot doing this bugfix. types in Lean live in different "universes". you can be generic over those "universes"
Fix universe levels for CoeSort instance by gaearon · Pull Request #161 · teorth/analysis
This seems necessary for solving not_mem_self from 3.2. I presume it worked before but got broken by the epilogue-related changes. Test case theorem SetTheory.Set.not_mem_self (A:Set) : (A:Object) ...
github.com
July 9, 2025 at 12:27 AM
spent ten minutes debugging why an element's border was showing underneath another element despite the latter being fully opaque. turned out it was a hair on the screen. i only noticed after i scrolled the page a bit down
July 8, 2025 at 7:36 PM
claude code is giving me the courage to do things i would never do (preprocess SVG illustrations for my blog with the gnarliest regexes to slightly tweak Excalidraw's output)
July 8, 2025 at 6:59 PM
ok this goes hard
July 8, 2025 at 6:05 PM
yay! i just proved 2 = 3
July 8, 2025 at 5:25 PM
lmao i'm asking claude questions about how regularity prevents russell's paradox and claude is getting so confused it asked *me* to help it untangle it
July 8, 2025 at 5:17 PM
i would like a set of all sets that don't contain themselves, please
July 8, 2025 at 4:17 PM
beer tastes so much better after yoga
July 7, 2025 at 7:19 PM
food
July 7, 2025 at 1:18 PM
ok i didn't realize this before but it's kind of wild that in Lean, which is strongly-typed (!), the return type of a function can depend on the input values (can even be extracted to another function to be calculated). i guess that's obviously needed for proofs to work but it's still wild
July 7, 2025 at 12:27 PM
want my discover to think stuff like this about accounts i top-like
Created an autogenerated list of the accounts I've liked most this past month! (Top-level posts only)

Hoping this can serve as a sort of rolling starter pack for accounts I enjoy.
July 7, 2025 at 2:42 AM
lean got a refreshed website! lean-lang.org
Lean Programming Language
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.
lean-lang.org
July 6, 2025 at 6:12 PM
Reposted
Markus Himmel has written a blog post about how to write a simple imperative program in Lean and then how to verify that the program is bug-free.

markushimmel.de/blog/my-firs...
My first verified (imperative) program
One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a fir...
markushimmel.de
July 6, 2025 at 4:03 PM
facts
July 5, 2025 at 9:22 PM
new kae tempest album is apocalyptic as ever but at the same time very life-affirming? chorus goes hard
Kae Tempest - Forever (Visualiser)
YouTube video by Kae Tempest
www.youtube.com
July 5, 2025 at 1:14 AM
new kae tempest
Kae Tempest - I Stand On The Line (Visualiser)
YouTube video by Kae Tempest
www.youtube.com
July 5, 2025 at 12:35 AM
oh huh number only commit hash
July 5, 2025 at 12:28 AM
does claude code never "undo"? seems like as a human i often "undo to last checkpoint where things seemed to work better". would be nice to codify this without git commits
July 4, 2025 at 11:27 PM
has anyone tried making agents emotional? i feel like it would be nice to have some kind of a state machine that makes it more motivated to dig into something or kind of backtrack when it gets bored, vs getting excited at chasing the solution when it feels it's close etc
July 4, 2025 at 11:23 PM
uhh thanks claude. this is great
July 4, 2025 at 11:15 PM
ok so this is kind of very interesting. you need to actually "design" MCP tools to work well. for example the Lean one is actually getting helpful now that we're sorting the autocomplete output by relevance.

but then it might help to include extra hints into the output: github.com/oOo0oOo/lean...
July 4, 2025 at 10:39 PM