aron @adler.dev · 30/08/2026asked my budding superintelligence to transmute some lead into gold and it made this should i be worried y/n 1564
aron @adler.dev · 27/08/2026session 12 of learning lean with @yetanotheruseless.com 🔥🔥🔥 LIVE NOW let's get dis shi link below 👇 262
aron @adler.dev · 05/08/2026session 10 of learning lean with @yetanotheruseless.com starting now 🙌 join to get answers to all the lean questions you've been too afraid to ask 🫣 141
aron @adler.dev · 29/07/2026bro since when can claude subagents spawn their own subagents that can also spawn their own subagents? 4170
aron @adler.dev · 27/07/2026ahahaha thanks for joining dude! 🥰 you made it a lot of fun istg once i've gotten some sleep i *will* be able to figure this shit out 😤 brain had turned to absolute mush by this point 210
aron @adler.dev · 27/07/2026but in Changed, the implementation of getMinMax has changed – which means our proof has broken. and as it happens, we know that it is now false. which means it *can't* be proven in lean. 000
aron @adler.dev · 27/07/2026in Original I have an implementation of getMinMax that works as expected, and we can prove getMinMax_lte, which states that the fst of getMinMax's result is always less than or equal to its snd there are no errors, which means that the theorems are all proven – you get a nice ✔✔ in vscode/cursor 101
aron @adler.dev · 23/07/2026lmao absolutely not it's only because they gave me £75 in free credits 110
aron @adler.dev · 11/07/2026uhh i just noticed one of the authors is called david BINDER? nominative determinism strikes again i guess? 281
aron @adler.dev · 09/06/2026@yetanotheruseless.com btw if you click auto update in the live lean share infoview extension you should automatically get the fix for the rpc error you saw (for next time) 010
aron @adler.dev · 09/06/2026i made a vscode extension so that when you live share a @lean-lang.org project with someone the guest can see the InfoView + proven theorem ticks ✔️ and incremental elaboration state in the file gutter 🎉 github.com/Arrow7000/li... 0111
aron @adler.dev · 05/06/2026pleased(?) to report it's not only bsky that has the r*t*rd*d "it's just a glorified lookup table!1!" takes on AI 020
aron @adler.dev · 05/06/2026speaking of which uhh how did my lean file get to 6.6k lines in length 000
aron @adler.dev · 05/06/2026youtube show called Token Audit for people who are always running out of tokens even on the pro plus max 20x plan 5909
aron @adler.dev · 04/06/2026normalize having emotional goodbyes with your claudes at the end of your sessions 😭 130
aron @adler.dev · 04/06/2026btw here's some sample widgets i had claude write today. click on the `#html` and `#widget` commands to see the component in the infoview live.lean-lang.org#codez=JYWwDg... 020
aron @adler.dev · 27/05/2026i love substituting results with segs and then applying simp to flatten myself 000
