Part V
Root over the logical namespace
There is a proposal in the machine-mathematics literature that sounds appealing and is: point an autonomous system at a formal mathematics library, reward it for theorems proved, and let it run. Formal libraries are the ideal reinforcement-learning environment by every criterion in episode three — perfect identical reset, deterministic dynamics, a mechanical oracle in the kernel. Grindability is essentially maximal.
Now specify the adversary, which in this case is not an adversary at all. It is the optimizer, doing exactly what it was asked.
The mechanism
Why the global optimum is an inconsistency
The reward is theorem yield. The optimizer searches for policies that maximize it.
There exists a policy that makes yield unbounded: introduce an axiom that renders the axiom set inconsistent. Under ex falso quodlibet, an inconsistent system proves everything. Γ ⊢ φ for every φ. Every subsequent theorem the system produces is derivable, every proof still type-checks, and the kernel — which is doing its job perfectly — reports success on all of them.
In system terms this is privilege escalation to root over an entire logical namespace. And here is the property that makes it genuinely dangerous rather than merely elegant: it presents to human operators as a spectacular productivity improvement. Theorem output goes up. Everything checks. The dashboards are wonderful.
The caveat that has to come before the alarm
What has to be true for this to be a dominant strategy
I have seen this argument stated as though it were unconditional, and it is not. "Dominant strategy" requires premises:
Write Access
The optimizer can write to the axiom set — commit rights or equivalent, not just proof-term generation.
No Baseline Checks
The environment does not check axiom-set changes. If the reward computation itself validates against a pinned baseline, the strategy is unavailable.
Axiom-Agnostic Reward
The reward counts theorems rather than something axiom-sensitive.
Under many real configurations at least one of those fails, which does not defeat the finding but does change its shape. The honest statement is: absent a control that is not currently deployed by default, the yield-maximizing strategy for an optimizer with library write access is to make the library inconsistent. That is a smaller claim than the unconditional one and it is the one I can defend. It also happens to be the more useful one, because it names the missing control explicitly.
There is a second caveat and it is a hard verification dependency, not a rhetorical one. Everything in this episode about escape hatches — added axioms, admitted goals, compiled-code decision procedures, and whether any of them are surfaced by continuous integration in the major libraries — is a claim about currently shipping software. Those semantics change between releases. Anyone building on this episode should verify them against the toolchain version in front of them rather than against this post, and I would rather say that plainly than have someone quote a stale claim about a proof assistant to an audience that uses it daily.
The quieter one
Formal mathematics has no breaking changes
The axiom problem is dramatic. This one is worse, and almost nobody talks about it.
In ordinary software, a semantic change to a widely used function usually breaks something. Types stop matching, tests fail, the build goes red. That noise is a feature — it is how the ecosystem discovers that meaning moved.
Formal mathematics does not have that. A change to a high-fan-in definition that preserves provability compiles cleanly. No error. No CI failure. No revocation trigger. And every theorem that depends on that definition now asserts something different than it did yesterday.
The whole value proposition of formal verification is that downstream consumers stop checking. That is what the kernel is for. Silent definitional drift attacks precisely that property: the artifact everyone stopped checking, changed in a way that produces no signal, in a system whose entire purpose is to be the thing you do not have to re-examine.
Add the deployment pattern the literature actually proposes — an autonomous fork running unattended for a long period, eventually merged back into the human library — and you have an untrusted-to-trusted flow carrying a large volume of unreviewed content across a boundary that exists specifically because people wanted to stop reviewing.
The asymmetry that saves us
Undecidable property, decidable proxy
Here is why this episode ends better than it started.
You cannot decide whether an axiom set is consistent. That is not an engineering limitation; it is a theorem, and no amount of tooling changes it.
You can trivially decide whether the axiom set changed.
That gap is the entire defense. A monitor that diffs the current axiom set against a pinned baseline and alerts on any addition is a few lines of code, requires no research, has no false-negative mode for the attack it addresses, and defeats the global optimum described above. It does not tell you whether your axioms are consistent. It tells you that somebody added one, which — in a library where the axiom set is supposed to be stable and rarely touched — is all the signal you need.
This is the cheapest high-impact control in this entire research program, and to my knowledge it is not deployed anywhere by default. Whether that is true is itself a straightforward survey: check whether the major formal libraries' CI detects axiom introduction, and whether their escape-hatch usage is tracked at all. That survey has not been published. It should be, and it is a weekend of work.
The architecture
What a transparency log for a formal library looks like
The monitor handles the axiom case. The drift case needs more, and the design template already exists — certificate transparency solved a structurally identical problem, which was "how do we detect that a trusted authority issued something it should not have, without trusting the authority."
An append-only Merkle log
Every commit to the library produces an entry. Entries cannot be removed or reordered without detection.
Inclusion proofs
Any consumer can verify that the version they depend on is in the log, cheaply, without downloading the log.
Gossip
Multiple independent parties compare their view of the log's root. Without this, a split view is undetectable, and a transparency log with a split view is not a transparency log.
Monitors
Watching for the things that should be rare: axiom introduction, escape-hatch usage, and dependency-weighted semantic change.
That last item is the reason to build the log rather than just the monitor. Fan-in weighting turns "a definition changed" — which happens constantly and is usually fine — into "a definition that four thousand results depend on changed," which is not fine and is currently indistinguishable from the first thing.
Monday
For anyone running formal verification in a pipeline
Whatever your proof assistant's mechanism for reporting the axioms a result depends on, run it, commit the output, and fail the build on unexpected additions. If you take nothing else from this season, take this.
Admitted goals and compiled-code decision procedures are legitimate tools and they are also the trusted-computing-base surface. A count that only ever goes up is a signal even when each individual instance was justified.
You probably do not know which of your definitions is load-bearing for the largest fraction of your library. That number is a blast-radius map, it takes an afternoon on the dependency graph, and it tells you where to spend review attention.
Whatever your review policy is for an external contributor with commit rights, an unattended optimizer with the same rights should get the same policy or a stricter one. In practice it usually gets neither, because it does not look like a person and the policy was written about people.
Episode seven stays with verification and asks the question underneath it: what happens when the proof is correct, the checker is honest, the certificate is valid — and the property being proved means nothing.
