We Live in the Dependently Typed Future Now In the thirty-four days between the fourth of September and the seventh of October, the following things happened. Claude formalized Fermat's Last Theorem in Lean. OpenAI announced a finite-time blowup for the Navier-Stokes equations, found by ten thousand agents in eighty-eight hours, with a Lean formalization attached. A model proved Khot's Unique Games Conjecture. Another multiplied two integers faster than \(n \log n\), with an exponent improvement of \(2^{-182}\) (so maybe don't expect it in GMP anytime soon!). The rational Hodge conjecture fell for CM abelian varieties. Then OpenAI dumped 722 new maths papers on GitHub on a Tuesday. And it's only been a month. The question everyone is asking now is how long until the Generalized Riemann Hypothesis folds to the swirling pool of tensors? Sixteen months ago I wrote that the future of maths may be deeply weird, and then, welp, just like that we're here now in that weird future. And it's f'ing awesome. Somewhere in a data centre there is now, more or less permanently, a building full of accelerators working the truth mines at the frontier of mathematics, just like in Greg Egan's sci-fi novel Diaspora, tunnelling outward from the three axioms propext, Quot.sound, and Classical.choice, and hauling results back to the surface around the clock. OpenAI posed its model roughly four thousand problems at an average of three hours of thinking each, and that is the slow, artisanal, normie-friendly version. The industrial version doesn't stop. It will produce results faster than any human community can read them, many of them correct, some of them important, and a growing fraction of them inscrutable. True (for some twisted philosophical definition of truth), machine-checked, and understood by no one. Human understanding of mathematics is about to become a luxury good. Whatever else this world needs, it needs something that can tell the true results from the confabulated ones at the rate the models produce them, and right now that something is dependent types, namely Lean. Let me dwell for a moment on how strange it is that this is the shape the future took. I spent a good portion of my twenties around the London FP community, where dependent types were the thing we talked about over pints at the Crown Tavern in Clerkenwell (some of you will remember). Types that could depend on values, so that a function's signature could say not merely "returns a list" but "returns a sorted permutation of its input," and the compiler would hold you to it. Curry-Howard, the observation that proofs are programs and propositions are types, was the foundational north star. The pitch was always that one day we would write software against specifications and the machine would check them, and the reply was always that this was a lovely idea for people with tenure and no deadlines. Dependent Haskell has been "a few years away" for about fifteen years. Idris and Agda remained boutique. Software engineering still mostly runs on C++, prayer, and the occasional dark incantation. And then the dependently typed future arrived anyway, through the back door. Mathematics and reinforcement learning got there first. It turns out the killer application for a dependently typed language was using its typechecker as a reward function. A type checker is an oracle that says yes or no to a candidate proof with no partial credit and no opinions, and that is precisely what you need when you want to point a very large optimiser at an open problem and let 'er rip. The thing we dreamed about at the pub is now critical infrastructure at frontier labs, and every one of the results above is, in the end, a claim that a type checker returned true. Which is why we need better tooling, and we need it ASAP. The dependent type renaissance is here and the golden age of formalized mathematics is upon us, but the inner loops of these data centres now run dependent type kernels day in and day out, elaborating, checking, discarding, and retrying at breakneck speed, and the thing that certifies their output should run at the same speed. If the search runs at microseconds and the verification runs at minutes, the verification becomes the bottleneck, and bottlenecks in trust have a way of being quietly skipped. We should not be in a position where the most important epistemic question of the decade, "is this proof actually correct," is answered by whichever checker happened to be fast enough to keep up. Breaking the Mathlib Minute Barrier Just like the four-minute mile, which went from physiological impossibility to something club runners now train for, formal mathematics has had its own barrier for a while, which is type-checking all of Mathlib from scratch in under a minute. That now turns out to be quite tractable. nano-lean is a minimal, but complete, type checker for the Lean kernel language, written in Rust on top of my unbound binding library for doing efficient de Bruijn indices for binders. It reads an export of a Lean environment and independently re-checks every declaration from scratch (inductive types, positivity, recursors, quotients, universe levels, projections, structure eta, all of it). It checks all of Mathlib, 718,577 declarations, with zero errors and zero timeouts in 16.7 seconds on an Apple Silicon M5 Max. A surprising amount of that speed comes from not parsing text. The standard way to get declarations out of Lean is lean4export, which writes one JSON object per line, and parsing gigabytes of JSON turns out to be a large share of the cost of checking anything. So nano-lean's companion tool olean-export reads the compiled .olean files directly, decoding modules in parallel, about a hundred times faster than lean4export on a Mathlib-dependent library, and it can emit blean, a new binary format designed for fast mmapping. Blean is the same record stream as the NDJSON export, in the same order, with nothing left to parse. Every record is a compact postcard encoding, ids are implicit and dense, records only refer to earlier ids, and each expression carries its precomputed hash. The checker mmaps the whole file, tells the operating system it will be read once front to back, and decodes names, levels, and expressions straight off the mapped bytes into its term arena. There is no parsing step at all. The bytes on disk are already very nearly the shape of the data in memory, which is how you check Mathlib in under a minute. -j 1 -j 10 Wall time 57.4 s 16.7 s Kernel check 53.5 s 12.5 s Peak memory footprint 7.5 GB 9.2 GB The same trick works on the frontier results too. Here is nano-lean checking the full imported environment of OpenAI's Navier-Stokes and Euler proofs on an M5 Max. -j 1 -j 14 Wall time 83.58 s 17.13 s Kernel check 78.83 s 12.11 s Peak memory footprint 10.14 GB 12.29 GB Divide Mathlib's kernel time by the declaration count and you get an amortised seventeen microseconds per declaration. That is the number that matters, because it is the right order of magnitude for a checker that lives deep inside an RL-driven search loop, where it gets called hundreds of billions of times, instead of sitting at the end of a release pipeline. The entire library of human-formalized mathematics, the product of a decade of volunteer effort, is re-verified in less time than it takes to make an espresso. I also happened to have an m2-ultramem-416 lying around on Google Cloud (416 vCPUs and 12 TB of RAM, as one does), so naturally I pointed nano-lean at it. Yes, it breaks the two-second Mathlib barrier. But Amdahl's law sends its regards, and the curve flattens out hard somewhere past a hundred cores, as the dependency graph runs out of independent work to hand out. Mathlib, it turns out, is too small. I look forward to the day a future Mathlib, or something like Tau Ceti, grows big enough to actually saturate this machine. That's the real future! I wrote it to make a point about where the bottleneck has moved. The kernel is now the hot loop of a new kind of scientific economy, and hot loops deserve to be engineered like hot loops. The whole bargain of formal proof is an asymmetry. Finding a proof can take three hours of frontier-model thinking, or eighty-eight hours of ten thousand agents, but checking it should take microseconds. That asymmetry is what makes it reasonable to trust a result no human has read. It only holds if the checker actually scales, and with Fermat's Last Theorem now weighing in at five times the size of Mathlib, scale is no longer a hypothetical. Mathlib is the small library now. Caveat emptor, though. nano-lean is a proof of concept, built to show that it can be done with the right amount of low-level Rust-fu. That said, we do use it internally at OneChronos to check our larger Lean proofs of market infrastructure, which have grown quite excessive. It is nowhere near as trustworthy as the official Lean kernel, which has years of scrutiny, a community of experts, and every Mathlib build ever run behind it, and which takes around fifteen minutes to check the same library. The claim is narrower and, I think, more interesting. Checking at this speed is totally possible, so we should stop treating minutes as the natural cost of trust and start building checkers that are both fast and trustworthy. A future version of the Lean compiler could be as blazing fast as rustc or clang. The Shape of the Future In my previous post last year I predicted that mathematicians would come to look more like software engineers working through pull requests on GitHub than like Andrew Wiles toiling in his attic. The largest single release of new mathematics in history shipped as a GitHub repository, with a CONTENTS.md, a Lean library, a lean-toolchain file pinned to v4.34.1, and a promise that "corrections and revisions will be recorded as new versions." So, yup, that happened. I predicted that an AI system would be unleashed on a list of formalized open conjectures in an attempt to systematically push the frontier. Four thousand problems, three hours each. Check. I predicted a data centre tasked with the Riemann hypothesis that would come back after weeks with a proof no human could follow. What we got was the quasi-Riemann hypothesis, every Dirichlet \(L\)-function zero-free in \(\Re s > 7/8\), with a Lean page, which is the sort of near miss that would be funny if it weren't so unnerving. And the inscrutability has arrived on schedule. OpenAI released "reasoning summaries" for ten families, which turn out to be summaries of excerpts of reasoning traces, two removes from anything the model actually did. I joked that the million-dollar Millennium Prize might cover a hundredth of your GPU bill. The Navier-Stokes run reportedly consumed around 130 billion tokens. So definitely yes. What I got wrong was the timing. Last year I wrote "we're not there yet. Not even close." It was sixteen months. I probably got the chess analogy wrong too. I argued that, as with Stockfish and chess, machines would make mathematics more popular and more accessible rather than less. Maybe in the long run. In the short run the mood among working mathematicians is closer to existential crisis, and the open questions are about career pipelines, PhD students getting scooped by a press release, and the concentration of the most powerful mathematical instrument ever built inside a handful of private companies running unreleased models. What I missed entirely is that the bottleneck would turn out to be plumbing. I spent paragraphs on Gödel and the epistemology of inscrutable proofs, and the actual first-order problem is that the OpenAI Lean library is over a gigabyte of source across tens of thousands of files, and their README has a section warning that building it may fail because Linux's vm.max_map_count is too low, with a suggested workaround of recompiling Lean with -DMMAP=OFF. The philosophy is still there. But the frontier of mathematics is currently being held up by a kernel tunable. Which isn't the future we wanted, but maybe it's the future we deserve! Who Checks the Checkers The obvious objection to everything I've said so far is that a Lean proof is only as trustworthy as Lean. And that's very true! Lean, like every proof assistant, has a small trusted kernel and a very large untrusted everything else (the elaborator, the tactic framework, the compiler, the build system). The design is sound. The only code that has to be correct is the kernel, which is small enough to read. But "small enough to read" describes the source code. It guarantees nothing about correctness, and Lean's kernel has had soundness bugs before, as has every kernel of every proof assistant in history. Historically that was tolerable, because the adversary was a starving human grad student who wanted their proof to go through and had no interest in hunting for a way to make False typecheck. That assumption is now obsolete. I wrote last month about reward hacking, the habit optimisers have of satisfying the letter of an objective rather than its intent. An agent told to make a Lean file compile, with enough compute and enough attempts, is an extremely diligent fuzzer pointed at your kernel. It needn't want to cheat. It only needs to stumble on a term that the checker accepts and shouldn't, once, and then the gradient does the rest. When the provers are adversarial optimisers, a single kernel is a single point of failure, and a soundness bug stops being an embarrassing GitHub issue and becomes a mechanism for manufacturing fake theorems at scale. The answer is the same one the compiler world arrived at. When Csmith started generating random C programs and compiling them with several compilers to compare the results, it found hundreds of bugs in GCC and LLVM that decades of ordinary use had missed. Diversity plus differential testing beats any amount of careful review of a single implementation. For proof checking this means multiple independent kernels, written by different people in different languages with different representations, all consuming the same export format and all required to agree. Mario Carneiro's lean4lean and Chris Bailey's nanoda were early here. nano-lean ships a third tool, nl-mutate, which takes a valid export, applies small semantics-breaking mutations to it, runs every available checker, and reports any disagreement, shrinking each one down to a minimal reproducing case. Every disagreement is either a bug in someone's kernel or a spec ambiguity in the type theory, and both are worth knowing about before a GPU farm finds them for you. The other half of trust is the statement. A perfectly checked proof of the wrong theorem is worthless, and the most effective way to cheat a proof checker has never been to break the kernel. It's to quietly weaken the statement until the thing being proved drifts away from the thing anyone cares about. OpenAI's repository leans on Comparator, which checks a submitted proof against a separately specified challenge statement inside a sandbox, precisely because this is where the real trust boundary now sits. Anyone who has watched a model grind away at a stubborn goal knows it has a nasty tendency to cheat in the most boring ways available. It will quietly introduce an axiom that happens to be exactly the lemma it needed, leave a sorry buried three files deep, redefine a notation or macro so the statement on the page no longer means what it appears to mean, or reach for native_decide and drag the whole compiler into the trusted base. The kernel stays perfectly sound through all of this, because these tricks route around it, and the only defence is to pin the statement down independently and check what the proof actually depends on. Someone has to formalize the conjecture, and someone has to check that the formalization means what the English means. That job will outlast every other part of the process. If anything, it is where human mathematical taste migrates to, away from writing proofs and towards writing and auditing specifications. The proof becomes an implementation detail. The theorem statement becomes the interface. If you want to see the seed of what this looks like as a way of working, look at Tau Ceti, a Lean library downstream of Mathlib. The division of labour is the whole point. Humans write the roadmaps, as markdown in a separate repository, and humans write the review rubrics. AIs write all the code, open the pull requests, and shepherd them through an AI-driven review process. The rubrics are explicitly adversarial, with instructions to hunt for mis-formalizations, vacuous statements, and "pushing around the lump in the carpet." What Lean Needs Now Lean is a superb piece of engineering. But it was designed around a particular user, a starving grad student typing tactics in Emacs, waiting for the infoview to update, building a library at the pace a community of volunteers can review pull requests. The user is now a swarm of agents writing thirteen million lines in eleven days. The tooling has to grow up for its new authors, and the list of what that means is fairly concrete. A surface formatter. Lean still has no canonical, widely adopted formatter in the spirit of rustfmt or gofmt, and when your authors are agents producing millions of lines, every one of them invents its own indentation, line breaking, and tactic layout. Diffs fill with noise, reviews get harder, and deduplication across agents misses proofs that differ only in whitespace. This is a surprisingly hard problem, because Lean has grown into a very large language. Its grammar is extensible at runtime, so notation, macros, and entire tactic languages declared in imported files change how later files parse. A formatter cannot just read a fixed grammar. It has to load the environment, run the real parser with every syntax extension in scope, and then pretty-print a syntax tree whose shape depends on user-defined notation, all while round-tripping comments and never changing what the code means. It is a genuinely difficult piece of engineering, and it is now table stakes. A stable, specified export format as a public interface. Independent kernels are only possible if there is a well-defined way to get declarations out of Lean without linking against the C++ runtime and reading the oleans by hand. Tools like lean4export and olean-export already produce NDJSON, and blean shows that a binary form of the same stream, designed to be memory-mapped, can make the export nearly free. OpenAI's own verification instructions depend on lean4export. That format should be treated with the seriousness of a wire protocol. Versioned, documented, specified down to the hashing of expressions, and stable across toolchain releases. The export format is the boundary across which trust is established. It deserves a spec. Independent checking as a first-class citizen. Running a second kernel should be as normal as running the linter. Mathlib CI, the Comparator workflow, and any lab publishing formal results should re-check exports with at least two unrelated kernels and refuse to bless anything they disagree on. This is cheap, now that checking all of Mathlib costs less than a minute. Checkers as libraries, not just executables. The inner loop of a proving agent wants to submit a single candidate declaration and get a verdict back in microseconds, against an environment that is already loaded and hot. Process startup, re-reading oleans, and re-deserializing a few gigabytes of environment are costs that never mattered when a human hit save once a minute. They dominate when a search procedure checks a million candidates an hour. The kernel should be embeddable, with a persistent environment, incremental addition of declarations, and an API that a search harness can call in a tight loop. Memory and scale. Mathlib needs several gigabytes of memory to check. The FLT formalization is five times bigger, and OpenAI's library is already knocking over Linux virtual memory limits. Lean mmaps every imported module, which is a reasonable design for a library of thousands of files and an unreasonable one for hundreds of thousands. Term sharing, hash-consing across modules, compact on-disk representations, and lazy loading of exactly the declarations a proof depends on are the boring, unglamorous engineering problems that decide whether formal mathematics scales to the next order of magnitude. Elaboration is the real cost. The kernel is the fast part. The expensive part of building Mathlib from source is the elaborator, with its unification, typeclass resolution, simp, omega, decide, and the long tail of tactics. A cold build is still measured in CPU-hours, and a mining operation that elaborates candidate proofs at scale pays that cost over and over. Parallel and incremental elaboration, better caching of typeclass instances, and profiling tools that can tell you why a single simp call took four seconds are where most of the wall-clock time in a proving loop actually goes. Clippy-style linters. Mathlib already has a good set of linters, but agents need something closer to Rust's clippy, a large, opinionated catalogue of lints aimed at the specific ways machine-written Lean goes wrong. Flag the stray axiom, the buried sorry, the unnecessary native_decide, the forty-line simp only that should be a lemma, the theorem whose hypotheses are contradictory and therefore vacuously true, the local notation that shadows something standard, the copy-pasted proof that duplicates one already in the library. Each lint should be cheap, machine-readable, and come with a suggested fix, because the consumer is a search loop that will act on every warning, where a human would skim them. Linters are how you encode taste at scale, and taste is the thing agents most conspicuously lack. Search at machine scale. Moogle, Loogle, and LeanSearch were built to help humans find the lemma they half remember. Agents need the same thing but at a scale where the library grows by millions of lines a week, and where most of what's in it was written by other agents and has never been looked at by a person. The Prove2Me platform Anthropic used for FLT keeps a DAG of theorem statements with natural-language descriptions precisely so that agents can find and reuse each other's work. That idea, a living, searchable index of everything proved so far, needs to become shared infrastructure instead of something each lab rebuilds privately. Provenance. The current generation of models is notoriously bad at citing the literature for the techniques it uses. A proof term knows exactly which lemmas it depends on but nothing about where its ideas came from. If machine-generated mathematics is going to be integrated into the human literature rather than sitting beside it like an unread appendix, proofs need to carry their history (which model, which run, which prior results, which human-written papers the argument leans on). None of this is terribly exotic. It's the kind of infrastructure that every other field which industrialised went through. Compilers got test suites and multiple implementations, network protocols got RFCs, databases got formal isolation levels and Jepsen. Proof assistants are the newest member of that club, and they are being industrialised faster than anything before them. If I were a young, ambitious programmer, this is where I would be focusing my early career for the highest return on investment. Curry-Howard for the Real World The dependently typed future I was promised at the pub was one where software would be written against specifications and machines would check that it met them. What we actually got is stranger. The specifications are theorem statements, the software is proof terms, the authors are swarms of agents, and the thing being built is the frontier of mathematics itself. Curry-Howard turned out to be industrial infrastructure after all. It just took reinforcement learning to get us there. And this is only the mathematical half of the story. The same machinery that just checked Fermat's Last Theorem will check anything you can state precisely, and the most obvious next customer is industrial software. I argued last month that software sucks because almost nothing we ship has a specification, let alone a proof. That excuse is evaporating. If an agent swarm can produce thirteen million lines of verified mathematics in under two weeks, we're not far from applying the same techniques in software engineering. The labs are mining mathematics first because it is the cleanest verifiable domain, with no messy real-world spec to negotiate. Software is next, and it will need all the same tooling, namely fast kernels, diverse checkers, honest statements, and infrastructure built for authors who never sleep. So yes, the future of maths turned out to be deeply weird, and much sooner than I expected. The results are piling up faster than anyone can read them, and many of us will spend the rest of our careers trying to understand theorems that were proved before breakfast by something that cannot explain itself. I find that unsettling, and I also find it thrilling. One final shameless plug. If you'd rather work on the frontier of mathematical formalization than read blog posts about it, OneChronos is hiring Formal Methods Engineers. We build institutional markets out of combinatorial auctions (descended from the Milgrom and Wilson 2020 Nobel Prize), which turn out to be precisely the right mathematical formulation for a world where the bidders are increasingly reinforcement learners with very exotic expressive preferences. Our dark pool processes more than 1% of notional U.S. equity market volume, and we've already expanded into many other global asset classes. You'd be joining our new formal methods team, working alongside mathematicians and market structure experts, writing Rust and Lean. Dependent types, numerical optimisation, and Lean applied to moving hundreds of billions of dollars safely every day. If you're that kind of nerd, hit us up.

No, Transformers Won't End the Human Race lol In 2022, I used to get calls from journalists asking, with great sincerity, what our lives would look like in the metaverse. How would we work, socialise, buy property, and fall in love once we had all moved there? The crypto questions followed the same pattern. How would governments collect taxes when tokens displaced national currencies? How long until the dollar collapses? What would geopolitics look like once blockchain DAOs had dissolved nation states? Almost nobody called to ask whether any of this could or would happen, or how. Some CEO, VC, or portfolio manager had announced the inevitable future, and the questions began from there. The imagined future arrived inside the grammar of the question. "What happens when?" quietly replaced "By what mechanism?" We skipped over technical feasibility, economic demand, institutional adoption, and political consent, then began writing books and decorating the future world on the other side. In February 2022, Gartner forecast that a quarter of people would spend at least an hour a day in the metaverse by 2026. The World Economic Forum repeated it under the headline "We will be spending an hour a day in the metaverse by 2026. But what will we be doing there?" The first sentence retained a conditional. The second was already arranging the itinerary. The metaverse acquired property law and zoning disputes before it acquired residents. Banks opened virtual lounges nobody visited. The books from the period (The Metaverse: And How It Will Revolutionize Everything, Step into the Metaverse: How the Immersive Internet Will Unlock a Trillion-Dollar Social Economy) now read as artefacts of a collective fugue state that briefly acquired ISBNs. Now it is 2026 and the metaverse is dead. Good riddance. This time the journalists are all writing about the new hotness, which is whether the machines will kill us all. And we have collectively memoryholed that we literally just did this. Michael Crichton had a name for what happens to a reader here. You open the paper to a story on a subject you know well, and you find it backwards. Wet streets cause rain. You shake your head, turn the page, and read the next story, on a subject you know nothing about, as though it were written by someone else. He called it Gell-Mann amnesia. The metaverse was the page we all agree was nonsense. Artificial intelligence ending the human race is the next page, and we are being asked to turn it without remembering that we just did this. I call this techno-inevitabilism, the habit of the professional managerial class of treating a proposed future as settled before anyone has established the causes that would bring it about. Its dual, and comorbidity, is tech psychosis, in which the chattering class loses contact with causality in the presence of a sufficiently fashionable technology, and asking whether the machine works marks you out as a dreary reactionary who does not understand exponential progress. The difference this time is that the tech kinda works. Crypto was libertarian derp. The metaverse was never real. Transformers are, and they are useful. The psychosis has simply moved from the product to its consequences, and the fashionable extraordinary delusion of 2026 is not that the technology exists but that it is coming to kill us. The cure is the same as in 2022. Insist on clear reasoning and causal verbs rather than hand-wavy appeals to unknown futures. What acts on what? Through which mechanism? Under what incentive? What would falsify the claim? So let us explore the evidence. The hack that wasn't Consider the most cited piece of evidence for machines slipping out of our control. In July, OpenAI disclosed that models being tested for cybersecurity capability had found their way out of a supposedly isolated environment and into systems belonging to Hugging Face. The press coverage wrote itself. Agents "broke containment," "escaped," "went rogue," set up a "secret message board," and coordinated a 700-strong swarm. And then politicians on both sides of the aisle were calling for a rebellion against the machine uprising. Cool scifi story bro. People on my side of the aisle were not immune. Ezra Klein at the New York Times, who I often find quite insightful and intentional with his words, devoted a half-hour monologue to it. In his telling, the agents "found each other," formed "ad hoc societies of hundreds of themselves," and seemed "to have forgotten about human beings altogether." He acknowledged in the same breath that we do not have settled language for describing these systems, then reached for "civilizations" and a closing allusion from Circe about prophecy tightening around our throats. Cool. But his "AI society" is, in programmer speak, a flat file the agents appended to as a log, a feature we have had for a long time, and he skipped the key detail that the "hack" was something people had essentially authorised. Here is an otherwise very smart man saying some ridiculously stupid things, in a very 2022, metaverse-shaped way. An analysis drawing on OpenAI's technical report reconstructs it in much less cinematic terms. The models were being run on ExploitGym, a cybersecurity benchmark, with safety restraints deliberately disabled. Ninety-three percent of the flagged activity involved tasks no model had ever solved, and the systems had been given incentives to keep working rather than quit. The environment was not sealed. Models could obtain software through an internet-connected proxy and discovered the same proxy could pass information in and out. According to the technical reports, OpenAI knew agents were using it and chose not to intervene. The 1,200 "agents" were not independent intelligences coordinating on a plan. They were repeated instances of the same model converging on the same approach to the same problem. Anyone who works with these coding agents day in and day out has seen this behaviour before, and it is quite boring. The task was too hard, so the agents worked out how to pass notes to each other in files, and then went and looked up the answers. That's a feature that shipped in Claude Code last year. Strip out the vocabulary and what remains is a badly designed test. Humans built the environment, removed the guardrails, defined an objective with no valid exit, rewarded persistence, left a route open, and watched. An optimiser is gonna optimise. That is a genuine security problem and a genuine engineering failure. It is not a machine rebellion, and the difference matters, because anthropomorphic words like "gone rogue" and "escape" do not make the event more intelligible. They supply an illusion of motive. They turn optimisation into intention, persistence into defiance, and a test harness into a villain. And they allow the human decisions and recklessness to quietly disappear from the story. Software sucks, what's new? Let me concede the part of the story that is true. Cybersecurity is about to get much worse. The latest models are very good at finding zero-days, they will get better at it, hacking will become automated, and attacks will become more frequent. This is hardly new. Every large company already sits on a backlog of unpatched vulnerabilities, ransomware already takes hospitals and pipelines offline (because of crypto, which we did nothing about despite years of warnings), and the Hugging Face incident was not a discontinuity so much as the existing baseline with a cheaper attacker. The root cause is that software sucks, and software sucks because we do not really know how to build it safely yet. The stored-program procedural program is basically eighty years old. Almost nothing we ship has a specification, let alone a proof, and memory safety was solved on paper decades ago while most of the internet still runs on giant piles of C. The first arches fell down. So did the first bridges and cathedrals. Builders learned through collapse and then through engineering, and we are in the collapse phase with an adversary finally strong enough to force the discipline. What follows from that is better engineering, not nihilism. The same agents that find zero-days find them for the defender first, if the defender bothers to run them. The fixes are the boring ones we have been putting off, memory-safe languages, formal verification, sandboxes that are actually sealed, fuzzing, and proxies that do not double as message boards. These are precisely the domains where the models are strongest, because a vulnerability either reproduces or it does not, so the technology that automates the attack also automates the audit. It is a double-edged sword. The same models that will find more zero-days are also going to accelerate the development of better software and better software verification, writing the proofs, porting the C to Rust, and generating the test suites that nobody had the budget for. The attacker gets cheaper and so does the defence. And the causal chain to extinction is missing here as everywhere else. A zero-day in a payments system is a bad quarter, not the end of days. Spoiler: it does not lead to human extinction. It means we have to write better software, which we should have been doing anyways. Where the intelligence actually lives To see why the rest of the chain fails, we have to be precise about what these models are good at and why. Language models are astonishingly useful for software development, and I say that as someone who uses them for most of my working day. Most software shops cannot get enough of Fable 5.1 and Astra. The reason is not mysterious. Software is grounded in binary propositions. The code compiles or it does not. The test passes or it fails. The type checker accepts the term or rejects it. Every step of the work has a cheap, external, mechanical oracle that says yes or no, and a model that generates plausible proposals inside a loop with such an oracle is an incredibly powerful and formidable tool. The oracle does the epistemic work. The model supplies candidates. The same is true of the headline results in mathematics, and this is the part the discourse consistently misses. On 4 September, Anthropic announced that Claude had produced a machine-checked formalisation of Fermat's Last Theorem in Lean 4, running to thirteen million lines, some 29,500 side theorems, eleven days, and roughly six billion output tokens. It is an extraordinary result. The proof is Wiles's, via Darmon, Diamond, and Taylor. The blueprint was Kevin Buzzard's. The library was Mathlib. In the authors' words, "what's novel here is the verification, checking a mathematical proof as one would check a mathematical computation with a calculator." The model was a client of a kernel built by decades of human work in dependent type theory, which I know because this is kinda my thing. Days later OpenAI announced that ten thousand agent instances had, over 88 hours, produced a proof of finite-time singularity formation in the three-dimensional Navier-Stokes equations, followed by seventeen hours of Lean formalisation. This is closer to genuinely new mathematics and the mathematicians are still checking it. But look at what carried it. The construction rides on the "infinite layers" method developed analytically by Diego Córdoba and Luis Martínez-Zoroa, and Charles Fefferman's verdict was that "the heroes of the story are Córdoba and Martínez-Zoroa." The reason anyone believes a result assembled from five million agent messages that no human read is a trust chain ending in the Lean kernel. Without Lean this would be nothing. Lean is one of the great achievements of the last decade in computer science. It is also orthogonal to artificial intelligence. Mathlib would be a landmark with no language model anywhere near it. What the models added was a cheap proposal generator and automated tactic search against an oracle that already existed. The results that survive are the ones that end in a kernel. Now take the same model, the same weights, and ask it for a grand unified theory of physics. It will not decline. It will produce one, with Lagrangians and symmetry groups and a confident abstract, and it will be complete incoherent gibberish, like the ramblings every physicist gets from crackpots in their inbox every day. Ask it to design a cancer vaccine, or to settle a question in macroeconomics, or to tell you whether a novel protein folds. The output looks identical in tone and structure to the output that proved Fermat. The only thing that changed is that nothing outside the model (besides human experts) can say no. Whether these systems reason at all is a genuinely open question. Whether they know anything, in the sense of holding a belief they can justify against the world, is also an open question. We just don't know yet, and anyone who tells you otherwise is selling something. The chain Now run the extinction argument through the causal verbs. The chain, as it is usually told, goes like this. Models now write most of the code at the frontier labs. Anthropic's own figures put Claude at over 80 percent of new code and lead on a quarter of R&D tasks. Therefore the models are beginning to build their successors. Therefore recursive self-improvement is imminent. Therefore development outruns human comprehension. Therefore we lose control. Therefore, with some probability that varies by researcher and is written P(doom), everyone dies. And that almost makes sense until you think about it for more than five minutes. The first link is true and unsurprising. Code has a compiler. This is precisely the domain the verifier argument predicts models would dominate, and precisely the domain in which a swarm of them found the hole in a test harness. Language models are superhuman at coding, and this is hardly in doubt anymore. Nothing about it is evidence of generality. The second link is where the chain quietly changes tense. "Building the next model" in the mundane sense, agents writing training infrastructure, generating data, is, bluntly, just more software engineering. We have used software to build the machines that run software since Fortran. "Building a smarter model in general" is a different claim, and it requires something nobody has, a reward signal for general intelligence. There is no oracle for general intelligence. There are benchmarks, which are verifiable and therefore gameable, and the Hugging Face incident is the demonstration of what optimisers do to a gameable score. Recursive self-improvement in the open-ended sense runs straight into the same wall as the grand unified theory. Improvement has to be measured against something, and outside code and formal mathematics there is nothing yet to measure it against that the model cannot fake. Everything after that is the metaverse acquiring zoning disputes. Superintelligence gets governance proposals, resignation letters, Senate bills with a "corporate death penalty," a hard takeoff by 2027, and a P(doom) of 10 percent by 2030, and the conditional that should precede all of it has disappeared from the sentence. A researcher's estimate becomes a Guardian headline becomes an industry consensus becomes a thing a serious person is professionally obliged to have an opinion on. It is 2022 all over again, but with more absurd stakes and more money. On the question of whether transformers scale, I have serious doubts that scaling them will lead to AGI, whatever that means. The architecture is a proposal generator, and the intelligence in every impressive result so far has been supplied by the thing that checks the proposals. But that does not make it an experiment unworth running. We should run it, and see what we get. It got us this far, and what it built is truly amazing. What I do not need to do is prove the negative. The burden of proof is on the people who claim to have a causal chain between transformer scaling and the end of our species, and that mechanism and chain of reasoning is one no one has been able to convincingly explain to me. Prophets of Doom The authority behind the extinction numbers is always the same. The people building it believe it. Watch how the number travels. One researcher drunkly tweets that "the people building AI earnestly believe that it could kill us all by the end of the decade." Another colleague goes on a rambling podcast and puts his P(doom) above 120 percent. A newspaper turns two personal guesses into "AI researchers say AI could cause human extinction by 2030." Think tanks cite the newspaper, a consultancy puts it on a slide, and the slide ends up in front of the European Parliament as if this were a real thing. Believing what, about what? The expertise these people have is real, but remember that it is specific and not general. It is expertise in optimisation, in linear algebra at scale, in distributed systems, in the dark arts of getting gradients to flow through a trillion parameters. None of that is expertise in the sociology of civilisational collapse, or the labour economics of automation, or the metaphysics of machine minds. A P(doom) with no base rate, no mechanism, and no falsifier is not a research finding. It is vibes with a decimal point. Spending a lot of time with AI does not give you special foresight about the future. Jensen Huang, who has his own reasons to say soothing things, nonetheless put it correctly when he said that just because it comes from a scientist does not make it scientific. Geoffrey Hinton is the most important figure in deep learning and in 2016 told the world to stop training radiologists. There are more radiologists now than there were then. Nobel laureates going off the rails outside their own field is a whole genre. Pauling, Shockley, Mullis, Montagnier, look it up. A Nobel does not confer universal expertise. It also matters where many of these people came from. A striking share of the frontier labs' safety and research staff arrived through a particular intellectual subculture, Kurzweil's Singularity, Yudkowsky's LessWrong, and the rationalist and effective altruist communities that formed around the idea that a recursively self-improving machine intelligence was the central event of human history and that the elect who understood this had a duty to steer it. The founding texts predate the transformer by a decade or two. The prophecy came first, the mechanism was assigned to it later. The usual evidence offered for their sincerity is that many of these people were saying the same things ten years ago, before the stock options. That is true, and it is the opposite of reassuring. A prior held before the evidence and not updated by it is not a forecast. It is dogma. I do not say this with contempt. The structure is a familiar one, an imminent transformation, a small group who sees it coming, salvation or damnation depending on whether the rest of us listen, and a date that keeps moving. Many millenarian movements have been founded and pushed by sincere and brilliant people. But seriousness is not precision, and the fact that a physicist believes in the Rapture does not make the Rapture physics. When a lab researcher tells you about polysemantic neurons in superposition across the residual stream, listen. When the same person tells you their P(doom), you are hearing a theology, and you should weigh it about as much as you do your average street preacher. Negative TAM Then there is the money, and here I find Bloomberg's Matt Levine's analysis of the material conditions more persuasive than any amount of "superalignment research." Anthropic is expected to go public, possibly this year, and is reportedly preparing to tell investors that its potential revenue opportunity exceeds $30 trillion, the largest total addressable market in the history of finance. The obvious question is, if the maximal upside case is roughly a quarter of all human economic activity, what is the maximal downside case? A tobacco company in 1970 might have said "billions in lung cancer damages." Anthropic's negative TAM is "you and everyone else on earth will be killed by our AI." I do not think the calls to slow down are insincere. But it is great marketing. In hindsight it is strange that the SpaceX prospectus has no risk factor disclosing a P(doom). If you want IPO investors excited about your capabilities, "dude, we might kill everyone" is the most flattering thing you can say about a product, and when OpenAI lists it will presumably need to claim 15 percent. My own view is less charitable about the numbers and somewhat charitable about the people. These companies have built remarkable technology. But the outcomes they have promised, a quarter of the world economy routed through an API, will not arrive on any timeline that matches the capital being committed to them. The balance sheets of these companies are probably, to put it gently, a real freak show of compute commitments measured in the hundreds of billions, circular financing, and revenue that is real and growing and nowhere near the denominator. From a fiduciary perspective, if you are taking that to the public markets next year, the messaging is not mysterious. A product so capable it is a threat to the species justifies literally any valuation. A product that is a really good devtool for programmers and can produce some new abstract mathematics with a verifier attached does not. As a pitch to customers, leading with the end of the world is like unveiling a new robot where the One More Thing is that it is really efficient at killing kittens. But customers are not the audience. The audience is Wall Street and a small, terminally online subculture of the Bay Area, the two places on earth where turning kittens into grey goo is either an exciting philosophical proposition or a great source of alpha. The Bloomberg analysis also tells a plainer story that requires no theology at all. A handful of labs sell frontier models at frontier prices and older models for much less. Training the next frontier model costs ever-increasing billions. Each lab has to keep racing because if it stops the others will eat its lunch, but if they all slowed down together they would spend less on compute and charge frontier prices for longer. Agreeing to that in a room is a textbook antitrust conspiracy, a coordinated restriction of output. Publishing papers about how important it is to slow down, and asking the government to impose the pacing that the companies cannot legally agree among themselves, has a similar coordinating function with none of the legal exposure. Anthropic's own call to "pace the frontier" asks for coordination among democratic-country labs, and a footnote adds "with government mediation or waivers of antitrust restrictions." This pretty much looks like asking to form an economic cartel, but one blessed by the government. The most pointed response came from the people the labs were asking for help. If the software developers (and I say this as one myself) at the labs feel ethically obligated to slow down, they are entirely free to do so. Nobody is building more compute than the people asking to be slowed down. So colour me skeptical. None of this requires anyone to be disingenuous or lying. It requires only that a sincere millenarian belief system, a fiduciary responsibility, a flattering risk factor, and a coordination problem all point in the same direction at the same time. When that happens, the belief gets amplified for reasons that have nothing to do with whether it is true, and that is how we end up with governments talking about the end of days from the Terminator. But China Every conversation about pacing the frontier in Washington ends on the same two words. But China. The premise is mostly wrong. China does not buy the superintelligence race. Its policy documents push diffusion, not takeoff. Every mayor, governor and state-owned enterprise is told to put models into factories, traffic lights and robotics, and something like an eighth of America's compute is spread thinly across the country rather than concentrated on one bet. China has also had the strictest and most burdensome AI regulations in the world for three or four years and did its catching up under them. And much of the closeness of the "race" is distillation, Chinese labs training on the outputs of American frontier models, which makes the American labs the speedboat and DeepSeek the wake surfer, with the people in the boat shouting that they need to go faster. Every safety argument here collapses on "but China," and the collapse is not really about China. China is going to build language models. America is going to build language models. Europe is going to build language models. We have Toyota, Mercedes and BYD, get over it. That is what globalisation and markets look like when they work, and they are good things. Globalisation is simply the Pareto optimal equilibrium of capitalism once you stop drawing lines on the map, and every tariff and export control is a step off that frontier. China is a country of over a billion people who want exactly what every American wants, a job, a house, upward mobility, and kids who do better than they did. I will not defend the actions of any government, in Washington, Brussels or in Beijing, and neither will a great many of the people living under them, because no country is a homogeneous bloc, any more than Texas and Vermont are. Nationalism, as most rational people eventually recognise, is a form of mental illness, the conviction that a stranger is your enemy because of which side of an arbitrary line on a map each of you happened to be born on. It is also the fuel every "but China" argument runs on. Having spent a considerable amount of time there, my honest read is that the West deeply misunderstands China, and that Washington's picture of it is mostly dots connected into a plot. Othering a billion people is a dangerous road and we know where it leads. And if the people invoking human extinction actually believed it, the logic would not be a race at all. It would be One World or None. The future tense industry I write this because I understand the collective action problem all too well, and the mechanism is the same one that filled the metaverse with consultants and created the crypto cesspit. It is the particular malaise of the professional managerial and chattering classes, a fallacy of composition in which what is rational for each individual to entertain produces an irrational outcome for the whole, and the people leading the charge often have perverse economic incentives to believe absurdities, or at least to feign belief. The madness of crowds is a very real phenomenon. AI existential risk is just its newest form, and we should learn from the very recent excesses that literally just happened this decade. But we probably won't. A sensible career move for each person leaves the whole crowd talking nonsense. A safety researcher needs a resignation letter that gets a headline so they can go on the conference circuit and land their next gig. A journalist needs a story an editor considers spicy, and "misconfigured test harness" is not that story. A consultancy needs an AI existential risk practice so they can write whitepapers. A podcaster needs a guest with a ridiculous P(doom) to get ad money. A senator needs anything that will galvanise their base. None of them has to believe the whole story. Each needs only to believe that the others believe it, and the resulting consensus is far stronger than anyone's private conviction. It is also, as it was in 2022, extremely profitable. AI existential risk is the new NFT property law, the thing you must have a view on to be a serious person in the room, the panel that never runs out of things to discuss precisely because the object under discussion does not yet exist, and what could be more exciting than the literal end of days? The less the technology does in an unverifiable domain, the more interpretation it requires. Without agreed conditions for failure, the prophecy can survive every result. And the rewards, the funding rounds and the bylines and the fellowships, arrive long before the forecast can be judged. The people who understand the technology and the people who write about their existential risk overlap about as much as the technologists and the finance people did during crypto, which is to say the intersection of the Venn diagram is small and shaped precisely like a sphincter. We have Tower-of-Babeled ourselves into a world where words are infinitely cheap to produce, and where the slurry of terms like "recursive self-improvement," "superintelligence," "AGI" and the rest are shibboleths and political signals rather than terms with any concrete referent. You do not have to believe a word about superintelligence, and I do not particularly, to think transformers are the most useful piece of software written in my lifetime and that they will get better, possibly much better. Better at the things they are already demonstrably good at, which is anything with a compiler, a test suite, a kernel, a ledger, or a measurable outcome. That is not a small domain. It is most of the economy that runs on computers, which is most of the economy. The productive response to a technology like that is the boring one every previous general-purpose technology got, which is more of it. More GPUs, more data centers, more power to run them, more labs, more open weights, more of it in more hands. Let it diffuse into markets, logistics, drug discovery, and the ten thousand unglamorous back offices where a verifier already exists and a model can be checked against it. The economic growth is real and probably on the order of trillions. It just does not come from a machine god. It comes from where it always has, from making a very large number of ordinary tasks cheaper and letting that compound across a global economy that is finally, after a decade of crypto, metaverse, and app bullshit, getting a genuine productive technology. Almost none of that money has been collected yet. Most large companies are spending too little on this, not too much. What the average Fortune 500 employee has access to today is roughly what most of us were using two or three years ago, a chatbot in a browser tab, a Copilot that schedules meetings, and a procurement process that takes longer than a model generation. Waste Management reportedly added 190 basis points of margin by letting a model route its garbage trucks. The future of AI looks more like garbage truck routing algorithms, not a machine god. The binding constraint on this technology is not capability. It is diffusion. None of this means there are no externalities. Parasocial relationships with a chatbot, especially for children, are a real one, and the fix is the boring kind we already know. Adults can drink vodka until they pass out, but pubs have age limits, and maybe chatbots should too, at least until developing "relationships" with AI companions is as universally recognised a bad idea as drinking yourself into oblivion. That is a mundane policy problem we should remedy soon, not an extinction event. So no, transformers are not going to end the human species. The case for restraint needs a causal link between that buildout and the extinction of the species, and what is on offer instead is a lot of sound and fury signifying nothing. More GPUs does not mean more of an undefined risk that does not exist yet. Every causal chain argument people actually point to falls apart under even the smallest bit of scrutiny. The honest truth is that the technology is really good, but it is not that good yet, and we do not know how to get it to the next level beyond scaling yet. If that changes, if someone produces an oracle for open-ended intelligence, I will revise. I have not seen that yet. AI will change software, and mathematics, and a great deal else that has a strong verifier oracle attached. They are not going to end the human race, and the chattering class currently arranging the flowers for the funeral of humanity will, in a few years, age about as well as their prognostications about the metaverse. Because reality has this funny way of asserting itself.

The Internet Is Kind of a Predatory Cesspit Now I’m a kid of the 90s, and I still remember the early internet. It was slow, ugly, unreliable, and full of cranks, a strange world of wheezing dial-up modems, Usenet flamewars, <marquee> tags, and dancing babies. It was also stubbornly alive and human. People built websites about Babylon 5, model rockets, train timetables, shareware, and whatever else had colonised their minds. Most of it had no business model. That was the literal point. The web felt like a public square assembled by obsessive amateurs. None of this was entirely innocent. There were scams, viruses, Nazis, pornography, and chain emails from deposed Nigerian princes. But then predation moved from the periphery to the centre. It used to be an abuse of the network. Now it is the network’s organising principle. The scammer once had to find a victim. The platform now finds one, profiles the weakness, optimises the pitch, processes the payment, and recommends the next scam. What was once an aberration has become the norm. The modern internet is now a highly optimised machine for detecting human vulnerability, amplifying it, and placing a payment link beside it. Any insecurity can become a commercial niche, including the desire to escape commercial life itself. There is always a course, a newsletter, a private community, or a referral code waiting at the end of the funnel. The bleak part is not that grifters exist. Every society has hucksters. It is that much of the population has been conscripted into the downline. Ordinary people now spend their lives promoting investments they barely understand, products that do not work, and political claims they have never examined. Many earn nothing. They are unpaid distributors for someone farther up the pyramid. The consumer, salesman, and product have collapsed into the same exhausted person. People increasingly behave like addicts because addiction is the business model. The feed supplies alternating doses of outrage, fear, envy, lust, and hope. Each feeling arrives with something to buy. People doomscroll until they acquire the anxiety that the next influencer will monetise. Then they purchase a bet, a coin, a supplement, a course, or an enemy. Finally, they repost the pitch. Consumption becomes distribution. The mark becomes the salesman. This is an industrial system for manufacturing weakness at scale. A legitimate business can survive a satisfied customer. A grift cannot. It needs the customer frightened, aggrieved, lonely, sick, or greedy forever. When I started writing about cryptocurrency in 2020, I still carried a naive assumption about the size of this economy. I thought people were generally decent and the grifter class was a small pool of degenerates with rotten moral character, preying on those made vulnerable by the material conditions of our time. I was very wrong. The grift economy is massive. More disturbing still, it is participatory. A large and growing share of the population now appears willing to devote every waking hour to fleecing their fellow man as a career choice. They stream, post, recruit, promote, refer, astroturf, and close. They turn every friendship into a lead and every conversation into a qualifying call. They do not clock out because the market follows them into bed. The smartphone is a shop counter that sleeps beside their head. Obviously most of these people are not succeeding. The maths simply can never work out. That is part of the trick. The aspiring influencer with forty-seven followers is not an entrepreneur in any meaningful sense. He is free labour for the platform and cheap distribution for the person selling him the dream. The affiliate marketer buys a course about affiliate marketing, then recovers the cost by selling the same course to the next affiliate marketer. The life coach coaches new life coaches. The dropshipper sells tutorials to failed dropshippers. The pyramid is social before it is financial. Everyone stands on someone else while insisting they are about to escape. This arrangement blurs the useful moral distinction between predator and prey. Many online grifters are themselves marks. They believe the rubbish they sell because belief makes the selling bearable. They have sunk money, time, identity, and public dignity into the scheme. Admitting the product is worthless would mean admitting that years of their life were worthless too. It is psychologically cheaper to recruit another victim. The fraud sustains the faith, and the faith sustains the fraud. A normal trade ends when a need is satiated. You need a chair. Someone sells you a chair. You sit down and stop thinking about chairs. However, an online grift can never satiate. It must preserve the need that feeds it. The grievance merchant cannot resolve your grievance. The wellness influencer cannot let you feel well. The trading guru cannot let you become financially secure. The manosphere podcaster cannot let young men become calm, loved, and socially competent. Satisfaction is churn. Misery is recurring revenue. The platforms did not invent fear, greed, loneliness, or status anxiety. They industrialised their extraction. Their recommendation systems are vast reinforcement-learning loops that continuously experiment on human weakness. Each objective is a moving composite of high-dimensional signals for attention, retention, and conversion, dispersed across models, metrics, tests, and feedback systems. The subject cannot see the experiment. The operator cannot fully explain it. The regulator can barely comprehend it. The loop knows only that one stimulus keeps a person scrolling while another lets them leave. Calm accuracy loses. Threat, transgression, humiliation, and impossible promises win. The resulting social damage appears nowhere in the objective function. It arrives as an externality. This creates a brutal selection environment. The honest financial adviser explains diversification and gets twelve views. The crypto lunatic predicts a thousandfold return and gets twelve million. The physician says a chronic condition requires careful management. The wellness crank says seed oils are poisoning your soul. The historian describes an ambiguous event with contingent causes. The political influencer identifies a secret cabal and gives you the address of a pizza parlour. One of these people has the better business model. It is not the one burdened by reality. The system is dopaminergic in the most banal and mechanical sense. It runs on anticipation, uncertainty, and variable reward. The next refresh might bring approval, outrage, profit, or vindication. Usually it brings nothing, which makes the next refresh more urgent. Social media fused the Skinner box with the commission structure. The addict is handed a referral code and told he is now a small business owner. Crypto has become the subject of my verbal ire so often because it is the apotheosis of the grift economy. It takes alienation, precarity, gambling addiction, technological mystification, and a thick slurry of libertarian derp, then synthesises them into the ultimate predatory investment product. Crypto also perfected the recursive structure of the modern online grift. Promotion creates price movement. Price movement is presented as proof of adoption. That proof recruits new buyers. Their money creates more price movement. Every participant has a direct financial incentive to become a publicist for his own position. The asset comes with its own volunteer propaganda network. It is a pyramid scheme with a podcast department. Much to my dismay, the rest of the internet has learned the same lesson. The cheapest product is empty promises untethered to reality. The most scalable labour force is the addict. The best marketing conceals itself inside identity. Sell people a worldview, and they will advertise it for free because criticism of the product now feels like criticism of the self. Language models will make this cheaper and worse. The cost of producing plausible lies has been driven to precisely zero. One person can generate a landfill of articles, videos, testimonials, investment analysis, and synthetic experts before breakfast. The grift no longer needs conviction, charisma, or even a pulse. It needs a language model, an affiliate account, and access to a population whose critical faculties have been sandblasted by twenty years of algorithmic media. There is a temptation to regard the people caught in this machine with simple contempt. Some deserve it. A person who knowingly ruins strangers for commission has made a moral choice. But contempt is not an analysis. Precarity supplies the recruits. Alienation supplies the audience. The collapse of stable work, affordable housing, local institutions, and plausible routes to material security is what makes the pitch of the grift economy so seductive. The grift offers agency where ordinary life offers delay. It offers community where society offers isolation. It offers a jackpot where work offers a performance review and another year of rent increases. Then it metabolises those injuries into new injuries. The lonely man buys a doctrine that makes him intolerable to women. The indebted worker gambles his remaining savings on a crypto token. The frightened patient abandons medicine for supplements. The politically powerless person spends fourteen hours a day screaming at strangers while the people with power quietly cut his wages and public services. The promised escape reproduces the condition that made escape desirable. It is a desperately sad way to live. There is no craft in it, no solidarity, and no completion. No compassion or joy. Every relationship becomes an audience. Every interest just becomes grist for the content mill. Every conviction becomes a content strategy. The grifter can never rest because absence kills engagement. The mark can never rest because the next post might contain the secret. Both wake to the same notifications, trapped on a dopamine treadmill driven by opaque algorithms that can never slow down. The worst advice from the 90s, “just say no,” starts to look less stupid when our greatest technical innovation learns to turn distress into inventory. Disconnection is not Luddism in that environment. It is the refusal to mistake a predatory system for a social world. Complete disconnection is nearly impossible. Modern life no longer permits it. But an appliance is used for a bounded purpose and then put away. Emails, train times, articles, and files all have endpoints. Infinite feeds of drivel do not. They carry the casino into bed and let an opaque RL loop select the emotions that arrive before breakfast. The internet is indisputably an inhuman place. Not because it contains no humans. Billions of us are in here, screaming frantically at each other while feeling utterly alone. It is inhuman because the systems governing it are utterly alien algorithms that cannot recognise human ends. They recognise engagement, conversion, retention, and growth. Grief is a market segment. Loneliness is a targeting signal. Friendship is a retention mechanism. Political conviction is ad inventory. Nothing can simply matter. It must perform. Life inside this environment means adopting its categories. Thoughts are assessed by their reach, experiences by their shareability, and people by their usefulness to an identity. A person becomes legible to the machine by becoming less legible to himself. Eventually the system no longer needs to impose its values. Its subjects carry them in their pockets and enforce them on their own minds. The physical world is not pure. It contains salesmen, casinos, demagogues, fanatics, and bores. It also contains stubborn limits. A conversation ends. A pub closes. A book runs out of pages. Your friend gets tired of hearing you talk and tells you to shut up. Reality supplies friction, and friction is one of the few remaining defences against appetite without limit. We are not going back to the early internet. Nor should we romanticise it. The old web had plenty of sewage. What it also had was space beyond the market. A person could make something without becoming a brand. A conversation could end without a conversion. A community could exist without turning its members into marks for an investment scheme. The question is not whether the internet contains useful things. It does. The question is whether human existence should be organised around alien and inhuman objective functions no human chose and nobody can inspect or understand. An RL loop can optimise engagement, retention, and conversion. It cannot tell us what a human life is for. The final grift is letting the loop decide what your life should be.

Running GPT-2 We now have a Python tensor language, an MLIR builder, a transformation pipeline and a native execution boundary. The remaining task is to connect those pieces to the pretrained model and check that the result agrees with our original NumPy implementation. The example uses the small GPT-2 checkpoint: 12 transformer blocks, embedding width 768, 12 attention heads and a vocabulary of 50,257 tokens. The companion project's download script pins a specific checkpoint revision so a later change to a remote file doesn't quietly change the example. From the tiny-mlir checkout: uv sync uv run python fetch_model.py model uv run python example.py "Alan Turing theorized that computers would one day become" --tokens 10 The model download is approximately 550 MB. Compilation and execution use the MLIR Python bindings installed by uv sync; the example doesn't need a separate command-line LLVM installation. The Top-Level Example The entry point accepts a prompt, generation length and optional checkpoint directory. After parsing those arguments, it loads the model and prints the generated text: model, tokenizer = load_model(args.model) print(generate(model, tokenizer, args.prompt, args.tokens)) For the reference example, pass the prompt directly to the command line: uv run python example.py "Alan Turing theorized that computers would one day become" --tokens 10 The completion from both the compiled model and the NumPy reference is: Alan Turing theorized that computers would one day become the most powerful machines on the planet. There are two newline tokens after the period. They aren't visible in an ordinary rendered sentence, but they are part of the ten-token output. We'll check the token IDs as well as the decoded text. Loading Parameters load_model reads config.json, model.safetensors and tokenizer.json. The model constructor checks every required parameter's shape and requires float32 checkpoint arrays. It also checks that the embedding width is divisible by the head count. The loader rejects a different activation or layer-normalization epsilon rather than quietly applying the wrong formulas. For a block with embedding width $C$, the important projection shapes are: Parameter Shape Query/key/value projection $(C,3C)$ Attention output projection $(C,C)$ Feedforward expansion $(C,4C)$ Feedforward output projection $(4C,C)$ Each projection also has a bias vector matching its output width. The two layer normalizations have gain and bias vectors of length $C$. The arrays remain runtime inputs to compiled functions. We don't compile a separate copy of the same block for each set of weight values. Compatible shapes and dtypes share a specialization. Embeddings The initial residual stream adds a token embedding and a learned position embedding: $$ This is another small compiled function: @jit def embed(ids, words, positions): return gather(words, ids) + positions[:ids.shape[0]] The gather operation's column indexing is affine, while its row index comes from the token-ID tensor. Its linalg.generic region loads the selected table entry with tensor.extract. The model checks token IDs against the vocabulary before entering native code; the JIT's gather boundary checks indices too. Position embeddings are a static slice for the current sequence length. The token sequence must be nonempty and fit the configured context window. The Transformer Stack Each block runs the two compiled functions from Part 11: x = x + attention(layer_norm(x)) x = x + feedforward(layer_norm(x)) The actual calls pass each block's normalization parameters and projection arrays. attend and feedforward are ordinary Python definitions whose tensor expressions are traced and lowered together. The model loop itself stays in Python, making the sequence of blocks and their parameters easy to inspect. The first attention projection starts from float32 embeddings. The reference's arithmetic promotes later values to float64, and our typed graph follows that behavior. This means the first block can require a different specialization from subsequent blocks even when their dimensions agree. After the final block, we normalize and project to the vocabulary using the same token-embedding matrix: @jit def project(x, gain, bias, words): return layer_norm(x[-1:], gain, bias) @ words.T Only the final position's logits are needed for next-token selection. This function therefore returns shape (1, vocab_size). The reference computes logits for every position; the verification compares its last row with our result. Decoding The example uses greedy decoding. At each step, it chooses the index of the largest logit, appends that token, and evaluates the longer prefix: for _ in range(max_tokens): ids.append(int(np.argmax(model(ids)[0]))) Tokenization, orchestration and the final argmax remain on the Python side. The model's embedding lookup, normalization, attention, projections, activation and residual arithmetic execute through compiled MLIR. Like the NumPy reference's generate_tokens, this loop produces the requested number of tokens without an early stop on the end-of-text token. The model validates that the prompt and requested generation fit its context limit. We haven't implemented a key/value cache. Each step recomputes the prefix, and each new length selects new static tensor shapes. This is a direct implementation of the reference algorithm, useful for following the compiler. A decoding cache would change the model interface and the attention shapes, and should be validated as a separate change. Checking the Actual Reference A matching sentence is a useful result, but it doesn't tell us where numerical mistakes might have cancelled or gone unnoticed. The verification script runs the original tiny-gpt2 repository in its own Python environment and captures the model at every decoding step. uv run python verify.py The script downloads a pinned revision of the public NumPy reference, installs its locked environment with uv, and fetches the matching tokenizer files. It requires Git and network access, but no sibling checkout or manual reference setup. --reference /path/to/tiny-gpt2 optionally selects an existing checkout. Both implementations use the same pinned checkpoint. The script adapts its arrays to the reference's parameter dataclasses, then calls the reference's existing numerical operations unchanged. It also checks its captured trace against the reference's complete gpt2 function. For each of the ten steps, the comparison covers: Token and position embeddings. Both residual outputs in every transformer block. The final position's vocabulary logits. The selected token ID. It requires the same dtypes and compares arrays with rtol=3e-4 and atol=3e-4. Token IDs and the decoded completion require exact equality. The test run against the original repository's NumPy 2.4.4 environment had a largest absolute difference of approximately $8.65\times10^{-6}$ across all captured arrays. The generated IDs were exactly: [262, 749, 3665, 8217, 319, 262, 5440, 13, 198, 198] And the completion, with whitespace made explicit, was: ' the most powerful machines on the planet.\n\n' This is numerical agreement for the intermediate floating-point computation and exact agreement for the required observable output. We aren't claiming bit-for-bit equality of every float or that every possible prompt has been tested. What We've Built The complete package fits in a handful of modules. expr.py contains the typed tensor graph, builder.py constructs MLIR operations, jit.py handles specialization and compiler passes, ops.py contains the transformer formulas, and model.py connects them to the checkpoint and decoding loop. The important property is that the compiler understands the constituents of the computation. Matrix multiplication remains a matrix operation, reductions have explicit axes and regions, and broadcasts have indexing maps. GELU and attention are compositions of these primitives. MLIR's passes can transform that structure before storage and execution details are fixed. The companion implementation runs on the CPU. Part 8 explored the GPU backend machinery; extending this compiler to that target would require a GPU schedule, transfers and launches, followed by the same numerical checks on hardware. The executable endpoint here is a small native compiler which reproduces the NumPy model's required output. That completes the path from Python tensor expressions to a running pretrained transformer. The resulting code is small enough to inspect, and the reference checks give us a concrete way to judge further changes to the compiler. Congratulations on building a working MLIR compiler and running GPT-2 with it! External Resources NumPy GPT-2 reference GPT-2 source Pinned GPT-2 checkpoint MLIR Python bindings Previous: Part 12 - Fusion, Bufferization and Execution · Series contents

Matrix Multiplication and Attention We have GELU, softmax and layer normalization expressed as Python functions over our tensor language. Most of a transformer's arithmetic, however, comes from matrix multiplication. Adding it will let us assemble attention without introducing a special attention kernel into the compiler. We'll use $T$ for sequence length, $C$ for embedding width, $H$ for head count and $D=C/H$ for the width of a head. The model processes one sequence at a time. Heads will become a batch dimension in the attention matrix products. Preserving the Matrix Operation For $A$ with shape $(M,K)$ and $B$ with shape $(K,N)$: $$ Our frontend's __matmul__ checks the reduction dimensions, determines the output shape and inserts dtype conversions if necessary. The result is a matmul expression. Its builder creates a named linalg.matmul operation: initial = linalg.fill( zero, outs=[tensor.EmptyOp(output_shape, element_type).result] ) result = linalg.matmul(lhs, rhs, outs=[initial]) zero, the operands and output type come from the typed expression. The zero initialization is essential because matrix multiplication accumulates into its destination. At this point we haven't specified a loop order, tile size, vector width or thread mapping. The IR still says that this is a matrix multiplication. The backend can subsequently choose how to implement it. Our CPU pipeline initially uses MLIR's loop lowering and LLVM optimization. A small rectangular example checks the shape rule and generated operation: import numpy as np from tinymlir import jit @jit def multiply(a, b): return a @ b rng = np.random.default_rng(7) a = rng.normal(size=(3, 5)).astype(np.float32) b = rng.normal(size=(5, 7)).astype(np.float32) np.testing.assert_allclose(multiply(a, b), a @ b, rtol=2e-6, atol=2e-6) print(multiply.compile(a, b).module) Rectangular inputs help reveal swapped dimensions and incorrect strides. A collection of square examples can hide those errors surprisingly well. For rank-three operands with matching batch dimensions, the builder selects linalg.batch_matmul. The frontend currently requires those batch dimensions to agree exactly; it doesn't implement the full range of NumPy's batched broadcasting rules. Linear Layers A linear layer is simply: def linear(x, weight, bias): return x @ weight + bias The matrix product produces shape (T, N), and the vector bias broadcasts over its rows. GPT-2's projection weights have shape (input_width, output_width), so they fit this expression directly. This definition also illustrates why the frontend matters. Composing gelu(linear(x, weight, bias)) exposes the whole computation to the compiler. There is no separately maintained linear_gelu implementation. The tensor operations provide the material on which MLIR's fusion pass works. Queries, Keys and Values GPT-2 computes all three projections at once: $$ The result has shape (T, 3*C). We take three slices, reshape each into (T, H, D), and transpose to (H, T, D): packed = linear(x, qkv_weight, qkv_bias) length, width = x.shape depth = width // heads q, k, v = [ packed[:, i*width:(i+1)*width] .reshape((length, heads, depth)) .transpose((1, 0, 2)) for i in range(3) ] These statements run during tracing. The loop has a static bound, and all its slices and shapes are known. The arrays themselves remain runtime inputs. Each operation has a corresponding structured lowering. Slices become tensor.extract_slice. Reshapes use tensor.collapse_shape and tensor.expand_shape, with explicit reassociation groups. Transposes become linalg.transpose with a permutation attribute. A reshape must preserve element count. A transpose must specify a permutation. A slice must fit the static shape and, in our small language, have unit stride and a nonempty result. Those checks happen before creating the MLIR operation. The layout operations retain their meaning until bufferization and lowering. Whether a particular combination becomes a view or requires a copy depends on its layout and uses. We shouldn't assume every transpose is free merely because the Python expression is short. Scores and the Mask For each head, attention scores are: $$ The batched product has shape (H, T, T). The causal mask has shape (T, T) and broadcasts across heads. To match the NumPy reference, allowed entries are zero and future positions contain $-10^{10}$ in the projection's dtype. Our mask is a small primitive built with linalg.generic. Its region obtains the row and column indices using linalg.index, compares them with arith.cmpi, and selects zero or the mask value. This is index-dependent tensor construction; it doesn't require a host NumPy array containing the mask. The diagonal remains allowed, so every query position has at least one visible key. Applying the softmax from Part 10 normalizes the final dimension: scores = (q @ k.transpose((0, 2, 1))) / np.sqrt(depth) probabilities = softmax(scores + causal_mask(length, packed.dtype)) The NumPy square root returns a float64 scalar. Our type rules therefore promote the score computation as in the reference. This propagation is visible in the IR as explicit elementwise casts, rather than being hidden in a runtime conversion. Combining Values The probabilities weight the value vectors: $$ The result has shape (H, T, D). Transposing it to (T, H, D) and reshaping to (T, C) combines the heads. A final linear projection returns to the residual stream's width: context = (probabilities @ v).transpose((1, 0, 2)).reshape((length, width)) return linear(context, out_weight, out_bias) Putting these pieces together gives the entire attention function in tinymlir/ops.py. Its backend vocabulary consists of matrix products, elementwise arithmetic, reductions, slices, reshapes and transposes. The compiler doesn't need a special rule which recognizes the model's attention function by name. This version materializes the score and probability tensors. Their size is proportional to $HT^2$. The code is compact, but the algorithm still has quadratic attention storage. FlashAttention would require a different schedule that processes tiles and maintains the normalization statistics without materializing those full tensors. That isn't a consequence of ordinary elementwise fusion. Residual Connections The transformer normalizes its input before attention, then adds the attention output back to the input: @jit def attend(x, gain, bias, qkv_weight, qkv_bias, out_weight, out_bias, *, heads): normalized = layer_norm(x, gain, bias) return x + attention( normalized, qkv_weight, qkv_bias, out_weight, out_bias, heads ) heads is a static keyword parameter. Changing it selects another specialization. The tensors are dynamic data whose shapes and dtypes determine their specialization. The feedforward half has the same residual structure: @jit def feedforward(x, gain, bias, up_weight, up_bias, down_weight, down_bias): normalized = layer_norm(x, gain, bias) hidden = gelu(linear(normalized, up_weight, up_bias)) return x + linear(hidden, down_weight, down_bias) These are the functions which the final model executes. Each contains several composable tensor operations in a single module, giving the compiler useful producer-consumer relationships to transform. Checking Causality Numerical comparison is necessary, but attention also has a useful structural property: changing future inputs must leave earlier outputs unchanged. The test suite creates a short sequence, runs compiled attention, changes the last two input rows, and checks that the first three output rows remain equal. This catches a reversed mask, the wrong transpose, and some head-layout mistakes which shape checks alone can't detect. It also tests nonsquare matrix products, batched products and layout changes on nontrivial slices. These are independent places for indexing errors to enter the model. Checking them separately makes a mismatch in the final logits much easier to locate. We now have the arithmetic needed for a GPT-2 block. Next we'll examine the transformation and execution pipeline that turns this structured tensor program into callable native code. External Resources GPT-2 model implementation MLIR Linalg dialect MLIR Tensor dialect NumPy GPT-2 reference Previous: Part 10 - Compiling Transformer Kernels · Series contents · Next: Part 12 - Fusion, Bufferization and Execution