## LESSWRONGLW

In the alternative algorithm for the five-and-ten problem, why should we use the first proof that we find? How about this algorithm:

A2 :=
Spend some time t searching for proofs of sentences of the form
"A2() = a → U() = x"
for a ∈ {5, 10}, x ∈ {0, 5, 10}.
For each found proof and corresponding pair (a, x):
if x > x*:
a* := a
x* := x
Return x*


If this one searches long enough (depending on how complicated U is), it will return 10, even if the non-spurious proofs are longer than the spurious ones.

I guess then it would have to prove that it will find a proof with x > 0 within t. This is difficult.