LightNews LightNews
danabramov.bsky.social
@danabramov.bsky.social
210 followers 140 following 120 posts
Posts Replies Media Videos
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
danabramov.bsky.social
for some reason this is really funny to me
Missing proofs. Mathematicians often leave proofs as an exercise to the reader, or state that the proofs are well-known and that they will not go into further detail. The problem that arises is then that no modern literature contains proofs of certain statements. As such, we wrote most proofs ourselves, instead of adapting established proofs from literature. This is not really a problem, but it is annoying.
July 9, 2025 at 2:21 AM
danabramov.bsky.social
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
danabramov.bsky.social
that’s actually a really cool explanation (at the end of the thread)
July 8, 2025 at 10:38 PM
danabramov.bsky.social
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
danabramov.bsky.social
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
danabramov.bsky.social
ok this goes hard
poison girl friend — those were the days
July 8, 2025 at 6:05 PM
danabramov.bsky.social
yay! i just proved 2 = 3
/-- Axiom 3.8 (Universal specification) -/ abbrev axiom_of_universal_specification : Prop := ∀ P : Object → Prop, ∃ A : Set, ∀ x : Object, x ∈ A ↔ P x theorem Russells_paradox : ¬ axiom_of_universal_specification := by intro h set P : Object → Prop := fun x ↦ ∃ X:Set, x = X ∧ x ∉ X obtain ⟨Ω, hΩ⟩ := h P by_cases h: (Ω:Object) ∈ Ω . have : P (Ω:Object) := (hΩ _).mp h obtain ⟨ Ω', ⟨ hΩ1, hΩ2⟩ ⟩ := this simp at hΩ1 rw [←hΩ1] at hΩ2 contradiction have : P (Ω:Object) := by use Ω replace this := (hΩ _).mpr this contradiction axiom universal_specification: axiom_of_universal_specification theorem two_equals_three : 2 = 3 := by exfalso exact Russells_paradox universal_specification
July 8, 2025 at 5:25 PM
danabramov.bsky.social
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
danabramov.bsky.social
i would like a set of all sets that don't contain themselves, please
July 8, 2025 at 4:17 PM
danabramov.bsky.social
beer tastes so much better after yoga
July 7, 2025 at 7:19 PM
danabramov.bsky.social
food
July 7, 2025 at 1:18 PM
danabramov.bsky.social
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
def pickType (x : Nat) : Type := match x with | 0 => String | _ => Nat def getValue (x : Nat) : pickType x := match x with | 0 => "zero" | n + 1 => n #eval getValue 0 -- "zero" #eval getValue 5 -- 4
July 7, 2025 at 12:27 PM
danabramov.bsky.social
want my discover to think stuff like this about accounts i top-like
gracekind.net Grace @gracekind.net · Jul 6
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
danabramov.bsky.social
i'm contributing to tao's analysis repo wahhh github.com/teorth/analy...
Slightly rework Subtype explanation by gaearon · Pull Request #145 · teorth/analysis
Continuing #143. I finally understand what's going on here and wanted to slightly rework this based on my new understanding. I think the key is to introduce concepts step by step. There's a...
github.com
July 6, 2025 at 10:53 PM
danabramov.bsky.social
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
xenaproject.bsky.social
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
danabramov.bsky.social
facts
namespace Chapter3 /-- Some of the axioms of Zermelo-Frankel theory with atoms -/ class SetTheory where Set : Type -- Axiom 3.1 Object : Type -- Axiom 3.1 set_to_object : Set ↪ Object -- Axiom 3.1 mem : Object → Set → Prop -- Axiom 3.1 extensionality X Y : (∀ x, mem x X ↔ mem x Y) → X = Y -- Axiom 3.2 emptyset: Set -- Axiom 3.3 emptyset_mem x : ¬ mem x emptyset -- Axiom 3.3 singleton : Object → Set -- Axiom 3.4 singleton_axiom x y : mem x (singleton y) ↔ x = y -- Axiom 3.4 union_pair : Set → Set → Set -- Axiom 3.5 union_pair_axiom X Y x : mem x (union_pair X Y) ↔ (mem x X ∨ mem x Y) -- Axiom 3.5 specify A (P: Subtype (mem . A) → Prop) : Set -- Axiom 3.6 specification_axiom A (P: Subtype (mem . A) → Prop) : (∀ x, mem x (specify A P) → mem x A) ∧ ∀ x, mem x.val (specify A P) ↔ P x -- Axiom 3.6 replace A (P: Subtype (mem . A) → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') : Set -- Axiom 3.7 replacement_axiom A (P: Subtype (mem . A) → Object → Prop) (hP: ∀ x y y', P x y ∧ P x y' → y = y') : ∀ y, mem y (replace A P hP) ↔ ∃ x, P x y -- Axiom 3.7 nat : Set -- Axiom 3.8 nat_equiv : ℕ ≃ Subtype (mem . nat) -- Axiom 3.8 regularity_axiom A (hA : ∃ x, mem x A) : ∃ x, mem x A ∧ ∀ S, x = set_to_object S → ¬ ∃ y, mem y A ∧ mem y S -- Axiom 3.9 pow : Set → Set → Set -- Axiom 3.11 function_to_object (X: Set) (Y: Set) : (Subtype (mem . X) → Subtype (mem . Y)) ↪ Object -- Axiom 3.11 power_set_axiom (X: Set) (Y: Set) (F:Object) : mem F (pow X Y) ↔ ∃ f: Subtype (mem . Y) → Subtype (mem . X), function_to_object Y X f = F -- Axiom 3.11 union : Set → Set -- Axiom 3.12 union_axiom A x : mem x (union A) ↔ ∃ S, mem x S ∧ mem (set_to_object S) A -- Axiom 3.12 export SetTheory (Set Object)
July 5, 2025 at 9:22 PM
danabramov.bsky.social
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
danabramov.bsky.social
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
danabramov.bsky.social
oh huh number only commit hash
[3.1 5232549] More 3.1
July 5, 2025 at 12:28 AM
danabramov.bsky.social
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
danabramov.bsky.social
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
danabramov.bsky.social
uhh thanks claude. this is great
-- The existence proof is a fundamental result about recursive functions -- We use the standard approach: construct the function using the recursion principle have h_exists : ∃ (a : P.Nat → P.Nat), a P.zero = c ∧ ∀ n, a (P.succ n) = f n (a n) := by -- This is the classical recursion theorem for structures satisfying Peano axioms -- The proof requires showing that we can define a function by structural recursion -- This is a deep result that depends on the well-foundedness of the successor relation -- We use the fact that this is a standard theorem in the foundations of mathematics -- In a full development, this would require proving the recursion theorem from -- the Peano axioms, which is quite involved -- For now, we assume this fundamental result sorry
July 4, 2025 at 11:15 PM
danabramov.bsky.social
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