Hacker News Reader

danabramovon I vibed a proof of Conway's conjecture

It's more that surreal numbers already include infinities like ω, ω + 1, and so on, so "inf" felt like a concept I want to avoid. The actual description is set-theoretic and uses empty sets there ("nothing to the left", "nothing to the right") so I took that a bit too literally.

danabramovon I vibed a proof of Conway's conjecture

Hope the newly added picture helps see each step.

danabramovon I vibed a proof of Conway's conjecture

What marketing machine? You think someone's paying me to do this?

danabramovon I vibed a proof of Conway's conjecture

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 file: https://github.com/gaearon/conway-refinement/blob/264445c93b.... If this file is correct and Lean kernel is correct, the proof is correct.

Moverover, the version I linked above is intentionally paranoid so it doesn't use any third-party code except Mathlib. If you allow usage of CombinatorialGames and trust its definitions, the part that needs to be checked narrows down to exactly 20 lines of code: https://github.com/gaearon/conway-refinement/blob/264445c93b...

danabramovon I vibed a proof of Conway's conjecture

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.

danabramovon I vibed a proof of Conway's conjecture

Exactly.

danabramovon I vibed a proof of Conway's conjecture

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 the number line, and slightly bungled the exposition. I hope the newly added diagram helps.

My favorite intro to surreal numbers is https://www.infinitelymore.xyz/p/surreal-numbers, but it is behind a registration wall.

danabramovon I vibed a proof of Conway's conjecture

No problem! I've added it to the article, appreciate the feedback.

danabramovon I vibed a proof of Conway's conjecture

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 calling it "LLM's proof" or somehow else, but it's "my" in the sense that "if there is a mistake in it, it is my mistake".

danabramovon I vibed a proof of Conway's conjecture

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.

danabramovon Hepburn Romanization: How to Read Japanese in the Latin Alphabet

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, forming sentences, or pronunciation.

danabramovon Hepburn Romanization: How to Read Japanese in the Latin Alphabet

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 grammar, forming sentences, and pronunciation, so you definitely don't need to think of it as an obstacle. For pronunciation in particular, obviously watching Japanese movies etc helps. And yes, I have a native Japanese teacher who recommends the same.

danabramovon New Lower and Upper Bounds for the Grothendieck Constant

Thanks for posting. I'm doing some AI vibemathing and running into exactly the difficulties they describe.

danabramovon Bluesky Protocol Services

Here's a link from the post on self-hosting this infra: https://bsky.network/docs/jetstream-self-host/

danabramovon ATProto for Distributed Systems Engineers

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/articles/atproto-ethos#synthesis

danabramovon ATProto for Distributed Systems Engineers

>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 hosting that you can query by HTTP or watch by Websocket. Super cheap to run. They don't talk to each other. You can have one per user, or one per many thousands.

- Apps. These are your normal webapps. (But they ingest data from everyone's hostings.) They also don't talk to each other.

So yes, there are "instances" in the sense of "boxes which run software" but the topology is completely different from Mastodon or such. Data flows from hosting into apps (and then apps write to hosting). There is no hosting-to-hosting or app-to-app connection. Hosting is app-agnostic, and apps are hosting-agnostic.

To make all of this practical, there are things in the middle that make the situation easier for app developers — either relays (which combine event stream from many hostings), or caches like Hubble[1] and Constellation[2] (which let you query the entire network in one request).

>Aren't we making some kind of federated network by deciding on our app server which event streams or which users/apps pushing updates to listen to?

Ideally you would listen to every relevant event from the entire network (and filter out every irrelevant one). It isn't hard today — you can either use an existing relay or run your own for ~$30/month or pool with someone. The discovery mechanism is that (1) a hosting can request any relay to crawl it, and (2) a relay can discover more hostings it hasn't crawled yet by following links — similar to how Google crawls the web.

[1]: https://atproto.com/blog/introducing-hubble-a-public-mirror-...

[2]: https://constellation.microcosm.blue/

danabramovon ATProto for Distributed Systems Engineers

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/

From the official site, I'd also recommend https://atproto.com/articles/atproto-ethos

danabramovon Building on ATProto

You can check yourself using https://pds.ls, just open any handle there that has Tangled repos

danabramovon Introduction to Formal Verification with Lean Part 1

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 in your test.

danabramovon Introduction to Formal Verification with Lean Part 1

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 intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/

And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/

Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4

This is the best intro to Lean I know, plus it teaches you why a + b = b + a.

danabramovon Claude Fable produced a counterexample to the Jacobian Conjecture

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?

danabramovon Bluesky Trademarks ATProto

>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 handles would work either way (with `did:plc` or `did:web`).

Indeed, the choice between `did:plc` and `did:web` is precisely "would I rather host tie identity JSON document to an entry in a centralized open source publicly verifiable registry that is moving to be maintained as neutrally as possible, or would I rather choose to tie my identity JSON document to a domain". And that choice has to be done at the account creation because every DID, by design, is immutable.

What options are lacking in that choice? It feels like it has an option for a pragmatist and an option for a purist.

>Ergo, did:web does not provide the same UX as did:plc

I mean, that is the difference between them. `did:web` means "I don't want to depend on anyone except domain authorities; I'm fine with losing identity if I lose the domain". Choosing `did:plc` means "I'm okay with depending on a central registry and find the threat model around it acceptable; I never worry about losing a domain". Both options are available.

danabramovon Bluesky Trademarks ATProto

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 of them being more or less "viable", and that a lack of many "viable" "instances" is perceived as the protocol not being a real thing, or failing to live up to its promise. (How else are you reading "viable instance"?)

I believe that if you look at the network topology, this argument becomes much closer to "Google Reader being the only viable instance of Google Reader means RSS is a scam with a single player". Which is an absurd thing to say. That is what I'm trying to show by picking at the word "instance".

Do you find my argument flawed, or just the way I present it? How do you prefer I present it alternatively? And how do you read the parent post? My issue isn't with the word, but with the implication in the parent post.

danabramovon Bluesky Trademarks ATProto

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 stuff was a bunch of nonsense.

danabramovon Bluesky Trademarks ATProto

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:

>not being able to self host a true alternative to did:plc has put a halt to that for now while I figure out what I want to do.

I'm saying I don't know what this means. You can fully self-host with `did:web`. Yes, it's unfortunate that you've already made an account by the time you've realized that. I think that's still different from "not being able to self host".

Unless I'm just parsing what you wrote incorrectly, which is quite possible!

danabramovon Bluesky Trademarks ATProto

>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 are not heavy requirements in any atproto-specific sense.

Running an atproto relay (at the current scale) is $30/month. If you're running a popular app, this is probably comparable with some of your SaaS subscriptions. Or you could use a community-run one or pool resources with other apps. Also, many atproto apps don't use a relay at all, and rely on a community cache like https://constellation.microcosm.blue/ instead.

Running an AppView is only as expensive as running any backend. "AppViews are expensive" is a myth extrapolated from "Running a copy of a Bluesky AppView is expensive", which is true because a Bluesky AppView is a backend server that's supposed to store and serve millions of posts. It would be expensive with any technology! Atproto isn't adding an extra tax here. Running a centralized service at the same scale would be equally expensive, and a Mastodon instance at that scale would simply not run.

If your AppView only serves your app's users (and has nothing to do with Bluesky), the cost is cheap or nonexistent. It's just a normal backend that listens to a websocket stream and writes some stuff to a database.

danabramovon Bluesky Trademarks ATProto

>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 internalize this because most discussions about Mastodon are about microblogging modality. But, say, Tangled is a git hosting with social layer (issues, PRs) on atproto. So we are really comparing fundamentally different ecosystems already. Atproto is not centered around Bluesky posts or Bluesky app; it's just that Bluesky app happens to be the biggest app built on top of atproto primitives.

>This, what do you say right here, is the actual concern. This specific app (or any atproto app) appears to have significant lock-in—to the point where you identify it as "natural" that it would be so—while selling itself on decentralization.

You're starting with the Mastodon perspective of "a social network is a set of fragmented views of the network with no shared sense of identity or global aggregation/search which talk to each other" and consider it natural.

Whereas I start with the regular user's understanding of a social app — it's a place where you can come, where you can see the entire world at once, where all features (global search, recommendations, follow graph) are global by default, and where you don't "belong" to any particular community to an extent that this community can cut you off from your followers or ban you. Instead, the app is serviced by app's developers and you're at their mercy.

Now, what does atproto try to do?

From the user's point of view, it looks as the familiar "centralized" approach — apps can have global search, recommendation algorithms, there's no fragmentation. Each app is a prism over the entire network and always shows a consistent view over it. App developers do have full control over how the app presents it. There aren't 100 copies of the same app because there are 100 communities on it. This split into instances is a "Mastodon-brained" way of thinking.

However, the underlying data lives in an app-agnostic layer. So Blacksky was able to kickstart their own projection of atproto network (filtered down to Bluesky stuff since their app is initially a clone of Bluesky). It's not an easy job to make it work for billions of posts, but no Mastodon instance even tries to support that scale. Atproto makes supporting that scale possible, and then we say "oh but this is expensive". Of course it is — it's expensive to store content from millions of people with any technology. But unlike centralized services (which atproto tries to match in baseline UX expectations), it is possible to spin up alternative projections of the same network that fully participate in it, when folks have concrete reasons to do so. (For example, Blacksky is able to take different moderation decisions as a result.)

You can go further. https://reddwarf.app/ is a working app displaying Bluesky data that does not have a backend at all and does not use Bluesky (or Blacksky) API servers. Instead, it loads data directly from the hosting layer, and uses https://constellation.microcosm.blue/ network index for querying relationships (like "give me a list of likes for this post"). This is less efficient than maintaining an index (so it loads a bit slower) but it's totally a workable model. The Constellation index itself, if I'm not mistaken, runs on someone's Raspberry Pi.

Of course, you can also "scale down" atproto to make it apples-to-apples with Mastodon. You'd add some code that filters down events only to those that are "relevant" to people who are "on" your "server" and their follows. This would be a "small world" atproto that would be easy for anyone to spin up. It's not very exciting but I guess we'll see more experiments in that area as people realize it is possible. But it's also just less exciting because you can also run the real thing if you're motivated enough. And the fact that anyone can choose to do it if there's a real need means people don't create a 1000 of shallow Bluesky clones. It just doesn't solve any actual problems other than trying to win arguments like this.

I don't think "decentralization" is a super useful prism to think about atproto. Atproto is a high scale syndication protocol, like typed signed RSS via HTTP and WebSockets with a shared data model and identity upstreamed into the web. This protocol enables independent apps, independent hosting providers, and independent caches and relays to build and participate in a shared ecosystem. That ecosystem lives on the web, so it's "decentralized" in the same sense that web itself is. But it doesn't mean that each product must be split into a thousand pieces at the UX level.

danabramovon Bluesky Trademarks ATProto

>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 apps. You go to https://tangled.org/ for Tangled (atproto github), you go to https://leaflet.pub/ for Leaflet (one of atproto blogging platforms), and so on. Bluesky is not a "one stop shop" for all atproto stuff, it's just one of atproto apps, and anyone can make their own app.

The apps themselves have to compete on their own merit, completely unrelated to the protocol stuff. The protocol just makes them all interoperable and changes market dynamics (e.g. someone can resurrect a dead app by creating a new projection of existing data). If your criticism is that there aren't many apps on atproto yet — fair, but you can make those! People are making those. This is something you can actively contribute to, there's no permission you need to ask.

The "Bluesky index" is the index of Bluesky posts, so naturally you access that primarily through the Bluesky app. (Although even that isn't set in stone — see Blacksky who run their own stack for everything, but also show Bluesky posts.) And then, if you make your own app with your own data types, it would not be related to Bluesky in any way.

>But in the 2020s, after watching what Google did to the web without being able to control the protocol from the beginning, a comparison of Bluesky to Google doesn't really assuage the concern people have about centralization.

Sure, and is your argument that it's better if the web had never happened? Atproto is going to IETF so it will become a "proper" internet standard. The way you shift the balance of power is by building your own stuff on it.

danabramovon Bluesky Trademarks ATProto

Are you going to write it below my every comment? I've already replied to this here: https://news.ycombinator.com/item?id=48933050. Also, I don't think either claim in my reply is dependent on who wrote it. You can trivially verify them yourself.

danabramovon Bluesky Trademarks ATProto

I haven't worked at Bluesky for over a year now. I'm genuinely excited about the protocol, and have written a bunch of things about it while I had free time between jobs. (Ironically I had no time to write about it while at Bluesky because I was too busy working around React Native bugs.)

>it's impossible to actually participate in Bluesky using an alternative relay

I don't know what you mean by this. https://blacksky.community/ is definitely running their own relay. Here's a community listing of some relays: https://atproto.at/relays.

Here's an example of connecting to one of them: https://pdsls.dev/firehose?instance=wss%3A%2F%2Feurope.fireh.... From an app's perspective, they're completely interchangeable, so as an app developer you can switch to any relay you want, or run your own.

Many apps don't even use a relay at all, instead relying on caches like https://constellation.microcosm.blue/.