Yes. My formulation was sloppy - I didn't mean "unless" to imply that there can't be a prover. My argument was that without a full prover, you won't have a usef

Yes. My formulation was sloppy - I didn't mean "unless" to imply that there can't be a prover. My argument was that without a full prover, you won't have a useful fitness function at all. And even then recall/precision need to be 100%. And even if you could achieve that, you still end up with something that... generates statements that are provably true. Mild yay. But that's not the problem. We can generate plenty of those. You want to identify the ones that actually advance the state of knowledge usefully.