Gödel machines, and what replaces the proof

Schmidhuber's Gödel machine is a program that may rewrite any part of itself, including the part that decides whether to rewrite, and does so only when it can prove, under its own utility function, that the rewrite is an improvement. The proof searcher is the whole construction. Everything interesting about the design follows from the fact that a self-modification is permitted by a proof rather than by a measurement.

This system departs from that, and the departure is stated at the top of the module rather than buried. We have no theorem prover and could not build one for this. The claim that wants proving here is not a theorem about arithmetic; it is a statistical claim about a distribution we only have samples from — that a particular adapter routes better than its parent. There is no proof of that available at any budget.

A certificate, not a proof

What replaces the proof is a certificate cheaper to refute than to produce, over content-addressed inputs, re-derivable bit for bit by any later run.

That is the right substitution because it preserves the property the proof was there for. A proof is valuable because anybody can check it without redoing the work that found it. So is this: the search is deterministic, the inputs are named by the hash of their contents, and the verdict is written down beside them. Any later run can take the recorded verdict and re-derive it, and re-deriving is far cheaper than the search that produced it. What is lost is certainty. What is kept is that nobody has to take the machine's word for anything.

Determinism is load-bearing, and its absence was the bug

Nothing in the training path is random. The adapter starts at all zeros, and a classifier-only variant does not move the cached features either. Both callers passed the same default budget.

So every trial trained a bit-identical adapter with the same content hash, and after the first adoption every later trial was comparing a variant against itself: nothing repaired, nothing broken, rejected. Forever. The loop ran every night and could not have improved anything, and from the ledger it looked exactly like a loop that was working and finding nothing.

The fix is not randomness. Determinism is precisely what lets a later run re-derive a verdict, which is the claim the whole module rests on, and a seeded search would have traded that away to fix a symptom. Instead a proposal names every knob it varies, and the search walks a declared grid in a fixed order, skipping points already marked as tried. The search is therefore re-derivable rather than merely repeatable: the next point is a function of the markers on disk, not of a coin.

Rendering is identity, so rendering is delicate

A proposal is identified by its rendering alone, which is why it renders floating-point knobs at six decimal places where a variant renders at two. At two places, a learning rate of 3e-4 and one of 2e-4 are the same grid point. A variant carries its adapter's content hash as well, so there the imprecision is cosmetic and the coarser rendering stays, because changing it would re-address every node already stored.

The same hazard has a sharper form. Adding a field to a hashed structure re-addresses every object that already exists, unless the rendering omits the field when the object omits it. An unconditional line for two later additions — whether a variant trained deeply, and which skill it adopted — would have re-addressed every node in every lineage, so the pointer naming the current best would have named something that no longer reproduced. The change meant to extend re-derivability would have broken it. Three self-test claims assert the omission rather than trusting it.

Adoption is a pointer swap

Every variant is a node, the parent stays addressed, and rolling back costs a pointer write. A line goes in the ledger either way, for adoptions and refusals alike, because a loop that only records its successes is a loop whose failure rate is unknowable.

Rolling back restores the routing rule too, but only when the two nodes disagree about it. Unconditional restoration would switch a lineage full of legacy zeroes to a rule none of those variants ever ran — the nodes recorded the proposal's rule rather than the rule in force, and every grid point carries zero while the machine has been running a different default throughout. Every node in every lineage therefore recorded a rule its variant was never measured under. That is fixed going forward and the old nodes cannot be fixed, so the restore is conditional instead.