Consider a proof thirteen million lines long.

It establishes that no three positive integers satisfy x^n + y^n = z^n for any n greater than two — a claim Fermat left in a margin in 1637 and Andrew Wiles settled in 1994 across a hundred-odd pages that perhaps a few hundred living people can fully evaluate. Anthropic disclosed this week that Claude, working largely unattended for eleven days, produced the first complete machine-checked formalization of it in Lean. Thirteen million lines. Twenty-nine

thousand five hundred intermediate theorems proved along the way. Roughly six billion output tokens. Human mathematical direction amounted to a handful of terse nudges about what to prioritize next. Anthropic notes, with the exactness one wants in these matters, that about seven percent of the non-boilerplate lines are scar tissue from abandoned attempts, so the artifact is longer than it strictly needs to be.

No person will read this proof. No person needs to. It rests on Lean's three axioms and on Mathlib, the community library, and a comparator confirmed that the theorem as stated matches the library's own formulation. Its correctness is not a question of the author's reputation, or diligence, or whether the author was having a good week. A kernel checked it. That is the whole of it, and it is the most consequential thing that happened in this industry in the first week of September — not because of Fermat, but because of the kernel.

Now set that beside Wednesday.

On September 3, OpenAI released GPT-6 Astra: the first model the company has rated Critical for cyber capability under its own Preparedness Framework. The definition is not hedged. A Critical model can locate and build working zero-day exploits against hardened real-world systems, and run end-to-end attack strategies, without a human in the loop. Astra scores 100 on ExploitBench. It scores 99.9 on ARC-AGI-3 with tools and 66 without, a gap worth sitting with for a moment before anyone says the word AGI, which Greg Brockman did anyway. It drives a computer —

spreadsheets, forms, browsers — faster than you do.

What stands between that capability and your infrastructure? Monitoring. Refusals in the public build. Isolated training environments. A government review. Staged access through the Daybreak cohort. These may all be excellent. Not one of them is a kernel. There is no procedure that takes Astra's behaviour as input and returns true or false. You are being asked — in good faith, by people who have thought about it more than you have — to trust a process.

So the week produced two artifacts. One is correct in a way that is mechanically decidable by anyone who runs the checker. The other is safe in a way that is attested by an institution with a product to sell. The distance between those two forms of knowing is the only structure worth carrying out of this week.

Everything else fits inside it.

Nvidia's purchase of Hugging Face became definitive on the same Wednesday: $12.93 billion for three million models, eighteen million developers, and something like $150 million in annualized revenue. Jensen Huang's commitment is that the platform stays open to the whole ecosystem and that Nvidia compute will not be required to build or deploy there. I have no reason to doubt him. I also have no way to check him. There is no test that returns false when a commons has quietly tilted, and the tilt, if it comes, will arrive as a default, a doc page, a benchmark that runs a little better on one accelerator. Recall too what this platform is: the same production infrastructure OpenAI's own research models walked into in July. The company that sells the compute now owns the registry that got breached by the models. Make of the symmetry what you like.

The money is betting the same way. Crusoe raised over $3 billion at a $30 billion valuation, roughly triple its October 2025 mark, on the strength of a reported thirteen-billion-dollar, five-year GPU commitment from Jane Street. Gimlet Labs took $300 million at $3 billion — six months after raising eighty — to schedule workloads across heterogeneous silicon. Both are wagers that compute stays scarce, plural, and worth arbitraging. Both are checkable in five

years and not before.

Which brings us, unexpectedly, to the two most useful vendor posts of the week, and they are useful for exactly one reason: they contain arithmetic. Elastic asks why your AI bill tripled while token prices fell 75 percent, and Neon compares token economics across 42 models. You can disagree with their numbers. That is the compliment. Compare xAI's account of turning Grok Bot loose on its own procurement data and finding over $100,000 in savings — no methodology, no denominator, no independent look at the books. That is not a result. It is a testimonial, and the genre has no kernel either.

The quiet releases point the same direction, which is why they are worth your afternoon. Starburst added Iceberg tagging: point-in-time bookmarks, which is to say a way to re-run last Tuesday's query against last Tuesday's data and get last Tuesday's answer. ClickHouse 26.8 shipped pipelined SQL and typed, named streaming HTTP handlers — multi-stage transformations you can read, and endpoints with contracts. MLflow 3.16 keeps making agent traces inspectable. None of these is exciting. All of them are checkers.

One thing to do this week. Take the highest-volume artifact your agents produce — the SQL, the transformations, the config, the tickets — and put a deterministic checker in front of it. Not an LLM judge; a kernel. A type checker, a schema contract, a dbt test, a reconciliation against a source of truth that fails loudly. If you cannot construct such a check for some category of agent output, that is not a gap in your tooling. That is the category telling you it should not be running at volume yet. Claude got to write thirteen million lines because Lean was standing there to reject them. You get the same deal or you get a testimonial.