gavinsyancey

Are there any registrars that are known to not do that?

No, that's the operations headquarters, staffed by people.

Aviation is generally used for longer journeys, and most of its risk is in the take-off / landing (so per-trip instead of per-mile). I wonder what happens if you compare fatalities-per-passenger-trip (or per-passenger-mile) on typical-length trips where aviation and HSR are competitive?

> deprecating it was also stupid. It was a legal decision made by Apple lawyers pursuing a particular litigation strategy vs Nvidia that caused Apple's withdrawal from Khronos group.

I'm not aware of the context here but that sounds like an interesting story. Could you give more details or do you know where I could read more about this?

LLM written.

Because they're longer, you can fit more doors on the side. If you allow all-door boarding, it's faster.

Not if you plan for double-deckers and put the lines higher up. And then single-deckers need a longer pickup pole.

Or more likely, an error in the formalization. "What you proved is true, but it's not sufficient for what you care about." See for example WPA2 KRACK attacks after WPA2 was proven secure.

> Imagine asking an AI to generate the whole numbers in order, from 0 on up. You could spend trillions of dollars having it fill up datacenter after datacenter with lists of numbers. The more we spend on the project, the more the list would start including some very big and important numbers. But what would actually be accomplished?

> Consider this and then consider how it applies to every number in any dataset and everything an AI generates: with our normal human understanding of a number, the number theoretically contains all of the meaning of that number. A number intrinsically contains the fact of whether it's prime, whether it's irrational, whether it's a counterexample to the Riemann Hypothesis, all facts known and unknown. You don't need a human to interpret the number in order for the number to mean what it means. In fact, the longer a human spends interpreting, the more meaning they might find that a number intrinsically has in and of itself. And yet... can you think of a less meaningful way to fill up a datacenter than with an ordered list of numbers?

> Listing all possible proofs out of context, whether in order or randomly, would hardly be more meaningful than listing numbers. Almost all possible proofs are trivial and meaningless, mathematicians select for the fun stuff.

> But I will say, since it seems every player in the US government and economy have committed to all jumping off a cliff together in a stubborn wish to cover the country in datacenters, I could think of worse applications than to fill them up with every possible mathematical proof below a certain size.

> You'd end up with a Library of Babel of proofs.

> You can imagine the quality of literature you'd get if you trained an LLM on the Library of Babel, which contains every possible book (or combination of characters that fit in 410 pages). The library, by itself, functionally contains no information whatsoever. The LLM trained on it would be a literal smooth-brain with no correlations to wrinkle up those gradients.

> Without the context of language and how it’s used by people, a great work of literature is just another possible random combination of letters. This can be represented as a point in multidimensional space, and a computer can guess that maybe there's more things of interest to humans near where the stuff we already like is, but only humans know how to push further into unknown directions of multidimensional space that are interesting and worthwhile.

> Whenever a company or person shares something “AI generated” that seems pretty good, that tells me that the AI must necessarily be using a lot of human-created data in that same area. The AI can not have leapt there on its own, even if it might look like it did to a person not aware of the scope of human-made work that went into it.

> The Mathlib of Babel problem is one reason why, in my view, formal math and AI are just one tool that might be useful for some math sometimes, not the end of mathematics or the future of mathematics. Formal mathematics and algorithmically-assisted proofs are not my personal aesthetic but I think it should be somebody's, and it's not like our fragmented field doesn't know how to handle another specific expertise joining the mix. We've already folded them in.

Found this interesting and thought-provoking. Why do we care about these proofs? Why do we care about this art, or this code? Because it is what is useful and interesting to humans.

Also, .internal was specified two years ago. .lan has been in use for decades.

This has been widely used since before there were any TLDs explicitly reserved for internal use.

.lan is widely used (by OpenWRT and Ubiquity and likely others) by home / SMB routers, where all connected devices will automatically be assigned hostname.lan. Technically, .home.arpa and/or .internal are designated for this, but .home.arpa is pretty clunky and they're very new (.home.arpa is from 2018 and .internal from 2024). Usage of .lan for this predates either.