I’m wondering how those proofs work and in which problems their conclusions are relevant. Trying more promising branches first improves efficiency in cases whe

I’m wondering how those proofs work and in which problems their conclusions are relevant. Trying more promising branches first improves efficiency in cases where you guess right, and wouldn’t sacrifice completeness if you would eventually get to the less promising choices. But in the case of something like a game engine, there is a deadline and you can’t search the whole tree anyway. For tough problems, it’s always a heuristic, incomplete search, and we’re not looking for perfect play anyway, just better play. So for games, that trilemma is easily resolved. And who says you can’t improve heuristics with better guesses? But in a game engine, it gets tricky because everything is a performance tradeoff. A smarter but slower evaluation of a position will reduce the size of the tree searched before the deadline, so it has to be enough of an improvement that it pays for itself. So it becomes a performance tuning problem, which breaks most abstractions. You need to do a lot of testing on realistic hardware to know if a tweak helped. And that’s where things stood before AlphaGo came along and was able to train slower but much better evaluation functions. The reason for evaluation functions is that you can’t search the whole subtree to see if a position is won or lost, so you search part way and then see if it looks promising. Is there anything like that in theorem proving?