## LESSWRONGLW

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