i guess this wouldn’t be very useful for blocking trolls. so it doesn’t cover all cases.

another funny idea is to reproduce mastodon’s “instances” model in that you have to choose one — and there can be mutual blocks between them — but no migration cost (because it’s “virtual” on top of atproto)

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

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.

for some reason this is really funny to me

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) ...

learned a lot doing this bugfix. types in Lean live in different "universes". you can be generic over those "universes"

that’s actually a really cool explanation (at the end of the thread)

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

> 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.

it's great you can talk to it like this though

does it do the job? yes. do i control all inputs? yes. off we go then

it did write a test suite, run my images through it, found and fixed a few bugs, etc. then deleted the suite (i don't think i want to maintain it). i guess i hope the suite was good, i never read it

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; }

like... whatever

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)

poison girl friend — those were the days

ok this goes hard

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)

from plato.stanford.edu/entries/russ... (h/t claude for the link)

i think actually this gives me a much better appreciation why Russell's paradox was a big deal. in this case the problem is obvious, but if you are even several inferences away from the paradox itself, you're still working in a system where you can technically derive anything

/-- 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

yay! i just proved 2 = 3

to be fair there was a "Retry with extended thinking" button and it did work

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

i would like a set of all sets that don't contain themselves, please

discover yes

beer tastes so much better after yoga

food

note this is not dynamic typing, everything is strongly typed. we're just deciding the return type... in another function

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

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

want my discover to think stuff like this about accounts i top-like

Slightly rework Subtype explanation by gaearon · Pull Request #145 · teorth/analysis Continuing #143. I finally understand what&#39;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&#39;s a...

i'm contributing to tao's analysis repo wahhh github.com/teorth/analy...

i think it's slightly tidied up but also a bit unbalanced, needs some work. there's zulip thread for feedback btw

screenshot from the page

apparently grind tactic is the shit

Lean Programming Language Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.

lean got a refreshed website! lean-lang.org

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...

i like what i like the bizarre type