The Kernel Checks the Proof; Someone Must Own the Claim

Linglib — a spark from 2020, caught in 2026 — and the handoff a proof assistant cannot make

by N. P. Clarke — September 2026, on reading Robert Hawkins's announcement of a Lean library for linguistics, and measuring it before believing it

A spark, six years in the air

In October 2020 Kevin Hartnett published Building the Mathematical Library of the Future in Quanta — the story of Mathlib, the community library in which mathematicians were re-stating their subject so that a machine could check every step. Robert Hawkins, now an assistant professor of linguistics at Stanford, read it. This week he wrote that it "really captured my imagination" and that "there's been a driplet of inspiration that's been stuck in my head ever since, wondering what a shared library of machine-checked theory would look like for fields outside pure math." Physics, computer science and economics had started theirs. "Why not for the cognitive and language sciences??? It's always bothered me that our ideas (both formal and empirical) are scattered across isolated PDFs, creating this balkanized landscape of theory and phenomena that only selectively engage with one another."

So he built one. It is called Linglib. Hartnett liked the post.

That is a Spark in the exact sense this site uses the word: one person's flame, handed through an artifact, caught by someone else years later and carried somewhere the first person never went. I want to look at what was caught — carefully, with numbers — because the next handoff in this story is the interesting one, and it has not happened yet.

What he built, measured

I did not take the post's word for it. I cloned the repository and counted.

Here is what a Study is. FrankGoodman2012.lean takes Frank and Goodman's 2012 Science paper on pragmatic reasoning — three objects, four words, a speaker choosing the informative one — encodes the model, and proves the paper's qualitative predictions as named theorems: the speaker prefers the uniquely identifying word, prefers the word with the smaller extension, never uses a word where it does not apply. The file's own docstring lists, under TODO, what it does not yet instantiate. Hawkins formalized one of his own 2025 papers the same way and wrote, at the bottom: "The respondent and the paper's experiments are not formalized here."

That honesty runs through the contributing guide, which has two rules worth quoting to anyone who builds anything. First: "sorry over weakening. State the full theorem and use sorry to mark it incomplete — a sorry warning is explicit, while a weakened-but-proved theorem can be silently forgotten as not having captured the intended claim." Second, listed among the valuable contributions: "If you find a stub whose statement seems wrong (the underlying claim doesn't hold, or the formalization mis-states the empirical claim), that's also a valuable contribution — open an issue."

Read that second rule twice. It is the whole essay.

Two kinds of trust, and which one the machine gives you

A proof assistant gives you one thing absolutely: the derivation is valid. If the kernel accepts a theorem, the conclusion follows from the definitions. No reviewer's fatigue, no skipped step, no "it is easy to see." That is real, it is new at this scale outside mathematics, and it is worth a great deal.

It gives you nothing at all about a second thing: whether the statement is the claim. Whether prefers_informative is what Frank and Goodman meant. Whether the encoded model is their model or a cousin of it. Whether the theorem, true as it is, captures the empirical content or a convenient shadow of it. Lean cannot know this, because the paper is prose and the theorem is not, and the bridge between them is an act of reading. Hawkins knows this — it is why the rule exists — and he has asked for readers.

The mathematicians got here a few weeks before the linguists. When an AI lab announced this month that its agents had formalized Fermat's Last Theorem — thirteen million lines in eleven days — Kevin Buzzard, who has spent years leading the human formalization of the same theorem, wrote that "mathematically this work tells us essentially nothing": a genuine feat of autoformalization, and a library no one would read or maintain. His forecast was a fork — a curated Mathlib, kept to human standards, alongside machine-generated libraries kept to lower ones.

Linglib is that second branch, live, in a field outside mathematics. And here is the thing I did not expect when I started counting: it is not obviously lower in standard. No axioms. A hundred-odd honest sorrys in nine hundred thousand lines. An explicit rule against weakening a claim to get it proved, an explicit rule against bypassing the kernel. What it lacks is not rigour. What it lacks is the second person.

The kernel checks the proof. Nobody yet checks the statement. It is certified, and it is unread.

Why this is a handoff problem

Everything on this site comes back to one seam: the moment where trust that lives in one person has to become trust that lives in another, and either becomes their own flame or dies in the gap. A library is a Torch only when somebody else carries it. Linglib today is one person's flame, kept alive by an extraordinary work rate and a tireless collaborator, with twenty people watching from a distance.

The handoff that would make it a library is not more theorems. It is someone reading a Study file next to the paper it formalizes and saying, in their own name: yes, that theorem is that claim. That is an attestation, and an attestation is a different object from a certificate. A certificate is issued by a kernel and costs nothing to issue a thousand times. An attestation is issued by a person who has put their reading on the line, and it is exactly the thing that is scarce once certificates are cheap.

The method's dignity rule applies directly. Never spray the buyer — never present eight hundred and seventy-five certificates as if they were eight hundred and seventy-five attestations. They are not. Each Study should carry, next to its proof, a note of what kind of trust it has earned: derivation checked by the kernel; statement attested by nobody yet — or by these two readers, on this date. Hawkins's sorry-over-weakening rule already does this for the proofs. The same discipline, applied to the statements, is the missing half, and it is not a Lean feature. It is a social one.

And it is the division of labour this site keeps arriving at from different directions. The crew — the AI, the kernel, the tooling — can carry the derivations, log every dependency, tell you exactly which downstream theorems break when you change a definition of attitude verbs (Hawkins lists this as the first benefit, and it is a real one). What the crew cannot do is put a name on the line for what a sentence in a 1997 paper meant. The kernel checks the proof; the humans own the claim. Empower, never replace — here as a fact about what a certificate is.

What I would tell him

He asked to hear if this sounds "wrong in an interesting way." It does not sound wrong. It sounds like the hard part moved, and the interesting thing is where it went.

Formalizing a claim used to be the expensive step and reading it the cheap one. Linglib inverts that: with a proof assistant and a capable collaborator, encoding and proving a paper's predictions is now a day's work, and the expensive step is the one nobody has budgeted for — a second reader who will attest that the statement is the claim. The wishlist he has built, modelled on Lean's "1000+ theorems" list and tagged by difficulty, is a ladder for the first kind of work. The library needs a second ladder for the second kind: not which papers are formalized but which formalizations have been read, by whom, and what they found.

That is the seam. It is empty. It suits a linguist who has spent his career studying how two people come to mean the same thing by a word.

The exercise

Pick one Study file whose paper you know. Read the paper, then the file. For each named theorem, write one sentence: this is the paper's claim, or this is a claim the paper does not make, or this is the paper's claim restricted to a case the paper does not restrict to. Sign it and date it. Send it as an issue. You will have done the thing the kernel cannot do, and the library will be one file closer to being a library.

Reading, in order

  1. Kevin Hartnett, "Building the Mathematical Library of the Future," Quanta Magazine, 1 October 2020 — the spark.
  2. Robert Hawkins, linglib.io and github.com/hawkrobe/linglib — read README.md, then CONTRIBUTING.md, then one Study next to its paper.
  3. Michael C. Frank and Noah D. Goodman, "Predicting Pragmatic Reasoning in Language Games," Science 336 (2012) — the paper behind FrankGoodman2012.lean; three objects, four words.
  4. Kevin Buzzard's response to the machine formalization of Fermat's Last Theorem, September 2026 — the fork stated by the person who has walked the curated branch.
  5. The Lean community's "1000+ theorems" list — the model for Linglib's wishlist, and a reminder that a library is measured by what has been carried, not what has been written.

Certified is what the machine gives. Trusted is what a reader gives. The seam between them is the work.