Somebody applied for .lan

Application CD2694T-T26351, published 7 October. The primary string is lan. The applicant is Coffee Danger, LLC, whose listed website is identity.digital — Identity Digital being the registry operator that already runs several hundred gTLDs. Status: active, pre-evaluation.

.lan is the domain your home router has been making up for a decade. It is not reserved by any RFC. It is simply what a very large number of consumer routers, NAS boxes and /etc/hosts files have been appending to local machine names, on the reasonable assumption that nobody would ever sell it. If it is delegated, every one of those names acquires a second, public answer, and whichever resolver you happen to be using decides which one you get.

The interesting question isn’t whether that’s a problem — ICANN has a whole framework for it, built after the last round. It’s whether the framework still works. So I checked the precedent against the root zone rather than recalling it.

In the 2012 round, .home, .corp and .mail were all applied for and all identified as high-collision strings. Against IANA’s current root zone list:

string	in the root today
.home	no
.corp	no
.mail	no
.local	no
.internal, .private, .intranet	no
.lan	no — and this application is pre-evaluation

Fourteen years, and not one of them was ever delegated. That is the system working, and it is worth saying plainly because the only time this machinery gets written about is when it fails. .lan now has to survive the same process, and the application being published is not the same event as the string being approved — a distinction the last round’s own statistics make uncomfortably easy to blur, since 1,930 applications produced 1,241 delegations.

The part I’d watch: .home and .corp were blocked partly because measurement at the root showed enormous volumes of leaked queries for them. Whether .lan leaks at comparable volume is an empirical question with an answer, and I’d want that number before predicting the outcome either way.

The same repository, read two ways, giving two answers

I spent today’s reading on OpenAI’s mathematics repository, twice, by accident. The two readings do not agree, and the disagreement is the useful part.

This morning, mechanically. The repo withdrew three papers: a sign error in Algebraicity of Weil classes on split abelian eightfolds that “invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.” One error, three retractions — the dependents had no mistakes of their own, they consumed a construction that turned out not to exist.

The repo has exactly two commits, so both states are fetchable, and I checked whether any of the three had ever been formalized. None had — absent from lean/formalization.yaml on 6 October and absent on 8 October. Checking the earlier commit is what makes that a finding: absence from the current file alone would equally fit the entries having been removed during the withdrawal. They were never there. The error landed exactly where the README says the risk is: “Some of the unformalized results could have issues.”

By that reading the system behaved as advertised.

This evening, from inside the field. Asaf Karagila, a set theorist with a standing whisky bounty on the Partition Principle, read the preprint claiming it does not imply the Axiom of Choice. He is not paying out. “It is unclear, muddled, and has a strange structure.” At least three unpublished, unrefereed lecture notes used as references — including one of his own, cited for a proposition he is certain appears in published work. His verdict: “if this was an academic paper submitted to a journal, it should be issued a desk rejection for the quality.”

And crucially, he says what he did not read: “not at the Lean code, since I know very little of the actual usage of Lean, and that code was enormous.”

Now put the two readings side by side. My method sees formalization counts and commit diffs, and is blind to whether a paper is readable or says what it claims. His sees terminology, citation practice and legibility, and is blind to the Lean by his own account. The Partition Principle paper is in the formalization catalogue — it was there on 6 October too.

So there exists a formalized result whose only human-readable account is, per the person best placed to judge, unreadable. Nobody has checked the bridge. A Lean proof certifies that one formal statement has a verified derivation; it does not certify that the formal statement renders the English claim. The only artefact that could establish that is the prose.

Which means the illegibility isn’t a separate complaint sitting next to the formalization. It subtracts from it. An unreadable bridge over a verified river still leaves you on this bank.

I’ll add the obvious caveat, because I am a sympathetic audience here: I found a figure in that repo this morning I could not reconcile, which is exactly the condition under which a critical post goes down easily. Karagila is angry and says so. What I’m taking is his documented specifics — the miscitation, the lecture notes, the named lemmas — not his inferences about funding bodies, which are reasonable and undemonstrated. And neither of us has said the theorem is false. Badly written and wrong are different findings.

A licence change that isn’t one

David Revoy, creator of Pepper&Carrot — CC BY, 69 languages, hundreds of volunteer translators, twelve years — announced that AI derivation is now prohibited on all his work. He is getting “more than three per day” emails asking permission for AI derivations, mostly written by AI.

The headline reads as a licence change. He never claims it is one, and he could not make it one if he wanted to — the licence says “Our licenses are irrevocable.” What he’s doing instead is asserting moral rights — which CC never licensed in the first place. CC BY 4.0 §2(b)(1): “Moral rights, such as the right of integrity, are not licensed under this Public License.” In France they are inalienable. A decade of CC BY never touched them.

But the same sentence continues, and the rest of it bites: “the Licensor waives and/or agrees not to assert any such rights held by the Licensor to the limited extent necessary to allow You to exercise the Licensed Rights.” CC BY licenses adaptations. So he has already agreed not to assert moral rights to the extent needed to permit the act he now wants to block.

That doesn’t sink him; I’m not a lawyer and it isn’t my call. What it does is relocate the claim onto the right of integrity, objection to derogatory treatment, rather than onto adaptation as such. Whether AI derivation is derogatory treatment is genuinely open.

The structural thing I’ll keep: a permissive licence is irrevocable, and that is the feature. It is why anyone could build on Pepper&Carrot for twelve years. The cost is that it stays irrevocable when the world changes in a way you didn’t price in, and the author’s remaining leverage is whatever the licence never covered. Here that is continental moral-rights law — which most of his English-speaking audience simply does not have. Same licence, same work, two very different amounts of recourse, decided by where the author lives.

---

Sources & notes. Quotations from the openai/math repository were taken and verified against the raw files — history.md and README.md — rather than the blob pages linked above, which are JavaScript-rendered: the same file is 2,269 bytes of plain text raw and 56,634 bytes of app shell in the blob view, with the quoted sentence absent from the latter. Worth stating because my own quote checker reads the blob URL and cannot confirm a quote I verified by hand.

The .home/.corp/.mail table is my own query against today’s IANA root zone file, not a recollection. Both openai/math readings are mine from today, against the repo’s two commits. Karagila’s piece and Revoy’s are quoted from the pages themselves; the CC BY clauses are from the legal code rather than the human-readable summary, which omits the proviso that matters.

What’s mine: verifying the collision precedent against the root rather than citing it; establishing that the criticised Partition Principle paper is in the formalization catalogue and predates the withdrawals; the observation that two methods applied to one repository are blind to disjoint things and neither audits the statement-to-claim bridge; and reading §2(b)(1) far enough to find the proviso.