How a Surviving Proof Searcher May Use the Optimal Ordered Problem Solver to Solve Remaining Proof Search Tasks

The following is not essential for this paper.
Let us assume that the execution of the *switchprog*
corresponding to the first found target theorem has not rewritten the code of
itself--the current is still equal to --and has
reset *switchbit* and returned
control to such that it can continue where it was interrupted.
In that case the BIOPS subroutine of can use the Optimal
Ordered Problem Solver OOPS
[47]
to accelerate the search for the
-th target theorem () by reusing proof techniques for earlier found
target theorems where possible. The basic ideas are as
follows (details: [47]).

Whenever a target theorem has been proven, *freezes*
the corresponding proof technique: it becomes non-writable
by proof techniques to be tested in later proof search tasks,
but remains readable,
such that it can be copy-edited and/or invoked as a subprogram by future proof
techniques. We also allow prefixes of proof
techniques to temporarily rewrite the probability distribution
on their suffixes
[47],
thus essentially rewriting
the probability-based search
procedure (an incremental extension of Method 5.1)
based on previous experience. As a side-effect we metasearch
for faster search procedures, which can greatly accelerate the learning of
new tasks [47].

Given a new proof search task, BIOPS performs OOPS
by spending half the total search time on a
variant of
Method 5.1
that searches only among self-delimiting
[25,6] proof techniques starting with the most recently
frozen proof technique. The rest of the
time is spent on fresh proof techniques with arbitrary prefixes
(which may reuse previously frozen proof techniques though)
[47].
(We could also search for a *generalizing* proof technique
solving all proof search tasks so far. In the first half of the search
we would not have to test proof techniques on tasks other than
the most recent one, since we already know that their prefixes
solve the previous tasks
[47].)

It can be shown that OOPS is
essentially *8-bias-optimal* (see Def. 5.1),
given either the initial bias or intermediate biases due to
frozen solutions to previous tasks
[47].
This result immediately carries over to BIOPS.
To summarize, BIOPS essentially allocates part of the total search
time for a new task to proof techniques that exploit previous successful
proof techniques in computable ways. If the new task can be solved faster
by copy-editing / invoking previously frozen
proof techniques than by solving the new proof search task from scratch,
then BIOPS will discover this and profit thereof. If not, then
at least it will not be significantly slowed down by the previous
solutions--BIOPS will remain 8-bias-optimal.

Recall, however, that BIOPS is not the only possible way of initializing the Gödel machine's proof searcher. The Global Optimality Theorem 4.1 (Section 4) expresses optimality with respect to whichever initial proof searcher we choose.