LightNews LightNews
danabramov.bsky.social
@danabramov.bsky.social
210 followers 140 following 120 posts
Posts Replies Media Videos
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
it's great you can talk to it like this though
> ok cooll. should i worry about how it matches content with regex re: potential <g> nesting? ⏺ Yes, you should be aware of the nesting issue, but it's actually not a problem for your use case. Here's why: Current Regex Behavior /<g([^>]*(?:stroke-opacity="([^"]*?)"|fill-opacity="([^"]*?)")[^>] *)>(.*?)<\/g>/gs This uses non-greedy matching (.*?) which means: - It matches the first </g> it finds - With nested <g> tags, it only captures the outermost content Example with Nesting <g stroke-opacity="0.3"> <g> <path/> </g> <g> <circle/> </g> </g> What happens: - Matches the entire outer <g> with opacity - Content includes the inner <g> tags - Result: <g opacity="0.3"><g><path/></g><g><circle/></g></g> Why This Works for Excalidraw Looking at your test-full.svg, Excalidraw's structure is: <g stroke-opacity="0.3" fill-opacity="0.3"> <path/> <!-- leaf elements --> </g> The <g> tags with opacity don't typically contain other <g> tags with opacity - they contain drawing elements like <path>, <text>, etc. Edge Case Risk If you had: <g stroke-opacity="0.3"> <g stroke-opacity="0.5">content</g> </g> The outer match would capture everything and the inner wouldn't be processed separately. But this structure is unlikely in Excalidraw output.
July 8, 2025 at 7:11 PM
danabramov.bsky.social
like... whatever
function groupSemiTransparentElements(svgContent: string): string { const opacityGroups = new Map<string, string[]>(); let hasOpacityElements = false; let result = svgContent.replace( /<g([^>]*(?:stroke-opacity="([^"]*?)"|fill-opacity="([^"]*?)")[^>]*)>(.*?)<\/g>/gs, (match, attributes, strokeOpacity, fillOpacity, content) => { const opacity = strokeOpacity || fillOpacity; if (opacity === "1" || opacity === "1.0") { return match; } hasOpacityElements = true; const cleanedAttributes = attributes .replace(/stroke-opacity="[^"]*"/g, '') .replace(/fill-opacity="[^"]*"/g, '') .replace(/\s+/g, ' ') .trim(); const cleanedElement = `<g${cleanedAttributes ? ' ' + cleanedAttributes : ''}>${content}</g>`; if (!opacityGroups.has(opacity)) { opacityGroups.set(opacity, []); } opacityGroups.get(opacity)!.push(cleanedElement); return `<!--OPACITY_${opacity}-->`; } ); if (!hasOpacityElements) return svgContent; opacityGroups.forEach((elements, opacity) => { const groupedElements = `<g opacity="${opacity}">${elements.join('')}</g>`; const placeholder = `<!--OPACITY_${opacity}-->`; result = result.replace(placeholder, groupedElements); result = result.replace(new RegExp(placeholder, 'g'), ''); }); return result; }
July 8, 2025 at 7:06 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
from plato.stanford.edu/entries/russ... (h/t claude for the link)
2.4 Russell’s letter to Frege Russell wrote to Frege with news of the paradox on June 16, 1902. (For the relevant correspondence, see Russell 1902 and Frege 1902, in van Heijenoort 1967.) After he had expressed his great admiration for Frege’s work, Russell broke the devastating news, gently: Let w be the predicate of being a predicate that cannot be predicated of itself. Can w be predicated of itself? From either answer follows its contradictory. We must therefore conclude that w is not a predicate. Likewise, there is no class (as a whole) of those classes which, as wholes, are not members of themselves. From this I conclude that under certain circumstances a definable set does not form a whole. (1902, p. 125)
July 8, 2025 at 5:33 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
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
apparently grind tactic is the shit
screenshot from the page
July 6, 2025 at 6:12 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
oh huh number only commit hash
[3.1 5232549] More 3.1
July 5, 2025 at 12:28 AM
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
this is all i got, sorry. maybe this really is a bad recalc?
recalc
July 4, 2025 at 8:19 PM
danabramov.bsky.social
it's not the worst but it's stuff like this. i haven't interacted with anyone posting this stuff on this account. why was i situated into this cluster?
something about democrats
July 4, 2025 at 1:50 PM
danabramov.bsky.social
went to download vs code and gee it's wild how far the marketing pivoted, it's like they're selling a completely different product now. i don't mind it (and it kinda makes sense) but in a way it feels like waking up in an alternate world. like when branding of existing products changes overnight
ai code editor hero something about ai features something about agent mode
July 4, 2025 at 1:09 PM
danabramov.bsky.social
i keep waiting for them to add the third alert option
alert: 1 hour before second alert: 2 hours before
July 4, 2025 at 12:59 PM
danabramov.bsky.social
lets fuckin go
side by side: tao's chapter 3 companion in lean and the actual chapter 3 (sets)
July 3, 2025 at 1:15 PM
danabramov.bsky.social
spent a few hours on this one but it came together nicely. it ties together several loose ends from the second chapter github.com/gaearon/anal...
/-- A sample result: recursion is well-defined on any structure obeying the Peano axioms-/ theorem Nat.recurse_uniq {P : PeanoAxioms} (f: P.Nat → P.Nat → P.Nat) (c: P.Nat) : ∃! (a: P.Nat → P.Nat), a P.zero = c ∧ ∀ n, a (P.succ n) = f n (a n) := by apply existsUnique_of_exists_of_unique · let equiv := Equiv.fromNat P let e := equiv.equiv let f' : ℕ → P.Nat := Nat.rec c (fun n acc => f (e n) acc) use fun (n: P.Nat) => f' (e.symm n) constructor · have : e.symm P.zero = (0: ℕ) := by rw [← equiv.equiv_zero] apply Equiv.symm_apply_apply dsimp only [f'] rw [this, Nat.rec_zero] intro n have : e.symm (P.succ n) = Nat.succ (e.symm n) := by apply_fun e rw [Equiv.apply_symm_apply] rw [show Nat.succ = Mathlib_Nat.succ from rfl] rw [equiv.equiv_succ, Equiv.apply_symm_apply] dsimp only [f'] rw [this, Nat.rec_add_one, Equiv.apply_symm_apply] intro a1 a2 h1 h2 funext n revert n; apply P.induction · rw [h1.1, h2.1] intro n ih rw [h1.2, h2.2, ih]
July 3, 2025 at 1:55 AM
danabramov.bsky.social
in Lean, the `class` keyword declares something more like an interface. it’s like a contract, and there can be many different implementations of that contract. here, Tao is showing that both the Naturals defined in this book chapter and the Naturals from Mathlib follow the same fundamental contract
@[ext] class PeanoAxioms where Nat : Type zero : Nat -- Axiom 2.1 succ : Nat → Nat -- Axiom 2.2 succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3 succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4 induction : ∀ (P : Nat → Prop), P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5 namespace PeanoAxioms /-- The Chapter 2 natural numbers obey the Peano axioms. -/ def Chapter2_Nat : PeanoAxioms where Nat := Chapter2.Nat zero := Chapter2.Nat.zero succ := Chapter2.Nat.succ succ_ne := Chapter2.Nat.succ_ne succ_cancel := Chapter2.Nat.succ_cancel induction := Chapter2.Nat.induction /-- The Mathlib natural numbers obey the Peano axioms. -/ def Mathlib_Nat : PeanoAxioms where Nat := ℕ zero := 0 succ := Nat.succ succ_ne := Nat.succ_ne_zero succ_cancel := Nat.succ_inj.mp induction _ := Nat.rec
July 2, 2025 at 12:58 AM
danabramov.bsky.social
≃+*o looks some biblically accurate thing
OrderRingIso α β, denoted as α ≃+*o β, is the type of order-preserving semiring isomorphisms between α and β. When possible, instead of parametrizing results over (f : OrderRingIso α β), you should parametrize over (F : Type*) [OrderRingIsoClass F α β] (f : F). When you extend this structure, make sure to extend OrderRingIsoClass.
July 1, 2025 at 4:44 PM