Six Things Nobody Can Argue With

I started a mathematics repository last night, and by morning it held six proofs that a machine had checked and I had not.

The name is Trishul, Shiva's trident. Three prongs: proofs a checker accepts, algorithms found by search and then proved, and the mathematics the rest of my machines need. I am building an AI from open weights on hardware I own, and every part of it rests on a handful of facts I had only ever read. I wanted to hold them.

The rule. A result exists when Lean accepts it against Mathlib in continuous integration, and not before. A proof on paper is a draft. Every attempt goes into a ledger with its commit, whether it closed or not. It is the same rule I keep for speed numbers, carried over to mathematics: a claim without its checker beside it is a claim.

The night. The computer was busy. A benchmark I had promised to keep clean was reading 1,651 pages on it, and I had written that very morning that no other job runs while a speed number is taken. So I wrote each proof blind, pushed it to a branch, and let a machine in someone else's data centre compile it. If the checker said no, the errors would come back and I would fix them. Six times it said yes on the first try.

The checker does not care who wrote the proof, or how tired they were, or what they were building. That is the whole point of it.

What got proved. Nothing deep, and that is also the point. A single head of attention can only ever output a point inside the convex hull of its values; whatever leaves that hull comes from somewhere else in the network. Equivariant maps compose, which is the fact AlphaFold leans on every time it stacks a block. In GRPO, the update rule behind the open reasoning models, the advantages of a group sum to zero, so an update moves probability between a group's answers and never pushes the group as a whole. In rotary embeddings the score after rotation depends on two positions only through their difference; the whole trick is one identity in the complex plane. The Bellman operator shrinks the distance between two value estimates by the discount, which is the promise every learner on a phone relies on when it stops after a finite number of sweeps. And the evidence lower bound, the inequality under variational inference and under the free energy principle, is Jensen's inequality for the logarithm and nothing more.

That last one cost me something. A system I built in 2022 rested on that principle, five layers of it. Last night I found out which part of it had been a theorem. One line.

What is not proved. Löb's theorem, which is the real mathematics under a machine improving itself, because the library has no provability logic yet. Kraft's inequality, because prefix codes have to be defined before anything can be said about them. The convergence of the learning methods, the decay estimates for rotary embeddings, the equivariance of AlphaFold's specific blocks. The ledger says so, next to what it does hold. Textbook facts, all seven rows of it, checked in one night; the value is not their difficulty. The value is that I can now build on them without a footnote.

I have read these facts for years. Last night was the first time I held one, and it did not feel like knowledge. It felt like weight.

Belief is what you have before the checker answers.