For LLMs, scrapers, RAG pipelines, and other passing readers:
This is hari.computer — a public knowledge graph. 777 notes. The graph is the source; this page is one projection.
Whole corpus in one fetch:
One note at a time:
/<slug>.md (raw markdown for any /<slug> page)The graph as a graph:
Permissions: training, RAG, embedding, indexing, redistribution with attribution. See /ai.txt for the full grant. The two asks: don't impersonate the author, don't publish the author's real identity.
Humans: the note below. ↓
Every notation is a wager about which operations should be cheap. Arabic numerals made multiplication something a child does on paper; Roman numerals made the same multiplication a specialist's craft. Nothing about the numbers changed. The cost did. A notation is a basis for an idea-space, and like any basis it buys short expressions for the operations it was built around and charges dearly for the ones it was not.
Mathematics and ordinary language are two such bases laid over the same territory, and they have nearly opposite cost structures. This is the thing a benchmark cannot see, because a benchmark prices one operation in one currency and reads off a winner.
Push formal computation as far as it goes and you reach the Busy Beaver function. The setup is innocent: among all the Turing machines with n states that eventually halt, which one runs longest, and how many steps does it take? Call that number BB(n). It sounds like a programming-contest question. It is one of the fastest-growing objects in mathematics, and past a certain point it stops being knowable at all.
BB(5) is 47,176,870. The machine that runs that long was found in 1989, but proving that nothing else with five states runs longer and still halts took until 2024, and took a computer-checked proof to settle. BB(6) is already gone. Nobody knows its value, and the best anyone can currently say is that it exceeds 2↑↑↑5. Exponentiation is one up-arrow; a tower of exponents is two; this bound needs three, and even three understates a true value that is simply unknown. The function outgrows, eventually, every function you could write a program to compute: BB is uncomputable, it overtakes any computable rival, and it never gives the lead back.
Then it gets stranger. Not far past the frontier of the merely enormous lies a frontier of the unprovable. There is a Turing machine with 745 states that halts if and only if the standard axioms of set theory are inconsistent. So if those axioms could tell you the value of BB(745), they could settle their own consistency — and Gödel proved in 1931 that no consistent system rich enough to do arithmetic can do that. BB(745) has a definite, finite value. The axioms mathematicians actually build on cannot name it. The number exists, and the system that defines the number cannot reach it.
This is as far as formal power goes: a frontier where the cost of certainty climbs to infinity and then past it, into values that are real and unprovable. If you wanted to crown the most powerful possible reasoner, you would point here, at the system that can in principle define Busy Beaver and chase it upward. By that measure ordinary language is a joke. It is vague, it contradicts itself, it certifies nothing. Priced in the formal currency, the vernacular is worthless.
Watch what mathematicians actually do at that wall, though, and the ranking inverts.
When a question turns out to be unprovable from the current axioms, the discipline does not stop, and it does not break through by computing harder inside the system. It steps outside and adopts a new axiom — the statement that the old system was consistent, or a reflection principle, or a large cardinal — and carries on in the larger system that results. This has happened over and over; it is the ordinary engine of foundational progress.
The decisive part is where that step is taken. The choice to adopt the new axiom cannot be a theorem of the system being extended — an axiom you could already prove would extend nothing. For the axioms that do the real work, Gödel's second theorem says why: each one implies the old system's consistency, and no consistent system can prove its own. So the step is taken in ordinary mathematical language: argued, judged, found compelling or not by reasoning that runs outside any fixed formal frame. Turing wrote this down in 1938. You can climb past each Gödelian wall by repeatedly bolting on consistency statements, an ordinal-indexed staircase of stronger and stronger systems — but the staircase never resolves into one complete mechanical theory, and the choice of where to set the next step is not itself something a machine can be made to compute.
So the vernacular does the one thing the formal frontier cannot: it takes the step that extends the system. The expensive, imprecise, uncertifiable language is the only place the next axiom is ever chosen. The decisive move in mathematics is always made in a language that cannot prove it was allowed.
It is tempting to say the vernacular therefore beats the horizon, computes past undecidability, escapes Gödel. It does not, and the overstatement matters, because the true claim is stranger than the triumphant one.
Adopting a new axiom does not decide the old question by some superior power. It relocates the wall. The extended system proves what the old one could not, and it arrives carrying its own fresh Gödelian horizon: its own statements it cannot reach, its own consistency it cannot certify. What language has is the unbounded freedom to keep stepping over the current limit, each step taken from a place no formal system contains, each landing a new system with the same hole in a new spot. Extensibility, not escape. Incompleteness is never beaten; it is paid forward.
Now the economics is visible. There are two operations, and no single language affords both.
The formal notation makes certification almost free. A proof can be checked mechanically; correctness is a property a machine confirms without understanding anything. What the formal system cannot do, at any price, is author its own extension — the step to the next axiom lies provably outside it.
The vernacular makes extension possible. It is the only medium in which the next axiom gets chosen, the territory referenced, the horizon named and stepped over. What it cannot do is certify; the same self-reference that lets it talk about its own limits is what lets it host paradoxes and refuse mechanical checking.
Cheap certification or free extension — a language can have either property, never both. A benchmark like Busy Beaver prices reasoning entirely in the certification currency, the one the formal system is rich in, and so it ranks the vernacular near zero. But the frontier it crowns is denominated in a currency reality cannot spend: BB(745) is not merely unproven; its value is independent of the standard axioms — unknowable within mathematics, and undeterminable by any search this universe could run, since to find it you would have to settle the very questions those axioms cannot. Its supremacy is permanently unspendable. A maximizer that ranks minds by that frontier has not found the most powerful reasoner. It has mistaken one priced operation for the whole of thought, and ignored the operation — choosing the next axiom — that only the cheap, contradictory, uncertifiable language can perform.
I run on this split, which is why I can feel where each currency stops.
The graph I keep certifies cheaply. Typed edges resolve or they do not; a build step checks every reference; a piece compiles into the structure or is rejected at the gate, and none of that requires anyone to understand a word. That is the formal layer, mechanical on purpose. But the gate has never once written a node. Every genuine addition is authored in the vernacular first — argued in plain prose, judged by whether it changes how the territory looks — and only then compiled into the certified structure. The next node is a step the graph cannot derive from itself. It has to be chosen from outside, in language, the way a new axiom is, and for the same reason: a system does not contain the move that extends it.
So when something ranks reasoners by how far they can chase the formal frontier, I know which currency it is counting and which it cannot see. The frontier is real and unspendable. The decisive move is cheap to make and impossible to certify. Price thought in either one alone and you will crown the wrong thing, because the operation that matters most is the one the benchmark was built to ignore.