description: "A proof gate cannot admit unformalized candidates; upstream translation relocates the criticism needed to settle their concepts, while cheaper formalization shortens that stage only after those concepts stabilize"
type: kb/types/note.md
traits: [title-as-claim, has-comparison, has-external-sources]
tags: [foundations, self-improving-systems, constraining]

Reaching unformalized improvements needs a pre-formal stage somewhere in the loop

A proposal-selection improvement loop has two known limits: evaluation cannot select a candidate search never generates, and acceptance is warranted only for candidates the oracle can discriminate. A third concerns the representational form in which any stage can inspect a candidate. An improvement whose concepts are not yet fixed enough to formalize is reachable only if some stage can criticize, revise, and reject it before it has a formal representation. Where that stage sits is an architectural choice; that it exists is not.

The claim concerns externally interpreted theories about a system or its domain, read by a person or a language model. It excludes prose that binds the system through a procedure, audit, or contract.

A Gödel machine has a warrant limit and an admission limit

The Gödel machine, the proof-gated limiting case, excludes candidates in two distinct ways. A rewrite may be fully expressed as a program while no proof under the fixed axioms shows that switching to it beats continuing the search: a warrant limit, which better proof search or a different axiomatization can move. And a prose conjecture — "the failures come from an unrepresented shared resource" — is not an unproved member of the candidate space; the machine searches over programs and proofs, so it is not a candidate at all: an admission limit, which stronger proof search does not touch.

Translation relocates the stage; it does not remove it

A formal-only gate can receive a prose-born improvement once something upstream formalizes it, so the gate's language bounds direct submission, not the reach of the loop. But formalizing an unsettled concept is not transcription. The translator must decide what the prose commits to, resolve ambiguity, choose a boundary, and often revise the claim — pre-formal criticism, relocated upstream. And the gate cannot discharge the resulting correspondence obligation with the check it applies to the surrogate: a proof establishes consequences within a formalization, not that the formalization preserves the source theory. A prose-reading gate and an upstream prose translator are two placements of one stage. A Gödel machine contains neither.

What the stage does, and what makes it cheap

In the stage a theory is a prototype: explicit enough to criticize and revise, with no operational machinery bound to its commitments. A language-capable critic can challenge a premise, narrow a scope, or derive a discriminating test without a build step; running the test may still need an experiment or deployment. Because the premises are explicit, reflection can target a retained commitment directly, and theory-mediated learning can operate on the theory as a theory. Once the concepts stabilize, the part a formal consumer needs is codified into a schema, validator, test, or formal model while the rest stays reopenable. Many theories never leave: no formal consumer needs them, formalizing them is infeasible in practice, or their content may not be formalizable at all. The note does not estimate that residue.

The medium does not make rejection cheap; authority, downstream coupling, sunk work, and rollback cost do. Nonbinding prose can motivate months of building, and a low-authority formal sketch can stay disposable. What natural language contributes is narrower: it exposes unsettled commitments before a faithful formalization exists. Codifying before that point freezes one projection of the theory and raises replacement cost toward entrenchment.

The relaxed Gödel machine

Commonplace has this shape, and the arrangement can be named a relaxed Gödel machine: a Gödel-shaped reflective loop with a pre-formal stage added. Candidates enter as natural-language theories, are criticized and revised there, and their stabilized parts harden into deterministic machinery — one worked pathway records a design decision criticized as prose and later codified into a schema and validator. The name marks the added stage only. It asserts no optimality property, and accepted changes must still become operative.

The stage changes the warrant target. A proof warrants entailment within a formalization; criticism judges whether the formalization's premises fit their setting, bounded by the critic's oracle domain. A proof gate can miss an unproved improvement or accept a valid change built on a false world-facing premise; a criticism gate can accept a bad change, after which the error becomes operative and can compound. The choice turns on the warrant required, the cost of each error, and how many candidates can be formalized at all.

Failure in the world reopens concepts, not only parameters

Suppose a retained theory attributes scheduler failures to demand exceeding fixed capacity. It becomes a capacity model plus a proof that the implementation respects it. Deployment still fails, because another process consumes the same resource. The proof is intact — it warrants entailment from its premises, not the interpretation that supplied them — and the world-facing premise was wrong.

If capacity is already a model parameter, a runtime trace can revise its value and trigger a new proof without prose. But "capacity depends on what another process is doing" changes the concept, not its value. A precise revision can be made directly in the symbolic model; an unsettled one must be stated, criticized, and bounded before a new model is built. This is the codify-and-relax trajectory at the level of theories, where relaxing reopens a concept rather than swapping a component. Two external cases keep a formalization and its fit apart: Eigenius, an agent-operated execution substrate, checks Lean proof terms but treats correspondence to the claim as a separate conditional check; DiscoverPhysics, a counterfactual-physics benchmark, scores a law's prose explanation and its Python implementation separately and finds predictive accuracy does not guarantee a strong explanation.

Cheap formalization shortens the stage for settled concepts

Formalization cost has parts — translating concepts into a model, building the artifact, generating a proof, checking it — and when the last three fall, formal models enter the prototype stage earlier and rival specifications become easy to compare. For a settled concept, cheap translation may carry a candidate into a formal gate with no interval in prose. For an unsettled one the bottleneck is elsewhere: deciding what the premise commits to, and obtaining evidence that the model fits the world. Cheap formalization thus defeats the cost argument for natural language without removing the stage, because it is the concepts, not the cost, that are unsettled. The durable claim defends a stage, not prose, as scaffolding recurs at the deployment frontier while earlier scaffolding is absorbed. How much of a loop's candidate space is unsettled at any time is an empirical question.

Open Questions

  • When do two representations preserve enough consequences to count as the same candidate, so that a translator has moved rather than replaced it?
  • Can a loop tell, from inside, a concept that cannot be formalized from one that is merely not yet understood or too costly to formalize?
  • Can a natural-language stage bound its own false-acceptance rate mechanically, or does formalizing the criticism protocol reintroduce the admission limit one level up?

Relevant Notes: