danabramov

7 ms·

31.
by danabramov 23d ago
Hope the newly added picture helps see each step.
32.
by danabramov 23d ago
What marketing machine? You think someone's paying me to do this?
33.
by danabramov 23d ago
Author here. No one's asking mathematicians to check the generated proof . I explain it in this part: https://overreacted.io/how-i-vibed-a-proof-of-conways-conjec... The only thing that needs a check is this 500-line
34.
by danabramov 23d ago
This procedure is enough. If you define addition and other operations in a certain way (as Conway did), it turns out that on the omega-th day (i.e. after initial infinite steps), all reals will be born.
35.
by danabramov 23d ago
Exactly.
36.
by danabramov 23d ago
I didn't want to introduce the notion of infinity because there are actual "infinite numbers" on the surreal number line. I've kind of tried to have both the simplicity of set-theoretic definition and the intuition of
37.
by danabramov 23d ago
No problem! I've added it to the article, appreciate the feedback.
38.
by danabramov 23d ago
Author here! My impression is that it's customary in the mathematical community to take responsibility for the result with your name, regardless of whether it came from LLM etc (as long as you disclose LLM usage). I am perfectly fine c
39.
by danabramov 23d ago
I made a picture, hope this helps: https://excalidraw.com/#json=zfKWWn1h7GzdFca6RDdXl,plr_WeaCt... Sorry it was confusing. Edit: the picture is now edited into the article.
40.
by danabramov 29d ago
Have you considered that different things are difficult for different people? Learning hiragana and katakana has taken me about a month, and I found it very difficult. There is no need to make it prerequisite for starting to learn grammar,
41.
by danabramov 29d ago
This is unnecessarily pedantic advice, and I encourage fellow learners of Japanese to ignore it. You will definitely need to learn hiragana and katakana but you can do it at your own pace, and it is orthogonal to learning the basics of gram
42.
A Proof of Conway's Refinement Conjecture in Lean(github.com)
2 points by danabramov 1mo ago|0 comments
43.
by danabramov 2mo ago
Thanks for posting. I'm doing some AI vibemathing and running into exactly the difficulties they describe.
44.
by danabramov 2mo ago
Here's a link from the post on self-hosting this infra: https://bsky.network/docs/jetstream-self-host/
45.
Bluesky Protocol Services(atproto.com)
213 points by danabramov 2mo ago|72 comments
46.
by danabramov 2mo ago
Some atproto designers come (somewhat disillusioned) from the p2p world, you can read what they have to say about that here: https://atproto.com/articles/atproto-ethos#peer-to-peer and https://atproto.com&#x
47.
by danabramov 2mo ago
>Yes, the user data is decoupled from the apps, but aren't both stored on some kind of instances? There are two main kinds of "nodes" in atproto: - Hosting aka "personal data servers" (PDS). This is dumb JSON h
48.
by danabramov 2mo ago
Shameless plug, but if this got you interested, I have a couple of longreads on the topic: - https://overreacted.io/a-social-filesystem/ - https://overreacted.io/there-are-no-instances-in-atproto/
49.
What Is the Atmosphere?(lab.leaflet.pub)
7 points by danabramov 2mo ago|0 comments
50.
by danabramov 3mo ago
You can check yourself using https://pds.ls , just open any handle there that has Tangled repos
51.
by danabramov 3mo ago
It works on the type system level instead of at runtime. So you don't actually need to "run" any code to verify it, and you can verify it for all possible inputs , even infinity of them, rather than for the ones that exist i
52.
by danabramov 3mo ago
Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/ Here's another article I wrote that gives some
53.
by danabramov 3mo ago
How much do you try to understand while doing it? I.e. how many levels of abstraction down in your own understanding do you go vs vibing at the surface level?
54.
by danabramov 3mo ago
>want to give people <usename>.<domain> account To clarify, do you mean you want their domain handles to look like this, or do you want to make them all have `did:web` identities? These are two different questions. Domain
55.
by danabramov 3mo ago
Let me try to explain my position. The parent post says "the only viable instance" which implicitly packs an assumption of Mastodon-like topology: a single product is expected to be split into many "instances", with some
56.
by danabramov 3mo ago
I'll try to mention it once per discussion page in the future. Also, I have not been working at Bluesky for over a year. While I was there, I was working on the client app and not the protocol. In fact, initially I thought the protocol
57.
by danabramov 3mo ago
I did read your post :) Yes, you can't migrate between PLC and WEB methods. It's not possible. I get that it's frustrating if you learn about it after making an account. Is that the whole concern? I was replying to this: &
58.
by danabramov 3mo ago
>If you want to run a social network on ATProto, you do need the relay and app view, and those are indeed heavy requirements, but the architecture is not the same, and it depends what you're actually trying to achieve. Note those
59.
by danabramov 3mo ago
>It probably is entirely true that different apps can spin up on atproto independently It's true, and I want to emphasize that they need nothing to do with microblogging or Bluesky posts. I think it's important to internali
60.
by danabramov 3mo ago
>designed it around their index as the primary means of accessing anything on the web That doesn't actually translate from the analogy though. You don't use Bluesky to access other apps' data on atproto, you use those

More ›