Comment by explaininjs

> you could enumerate all possible proofs of a given length

That does not help us with proof search as we do not know the target length.