The final state in chess is a single* state which yes, then branches out to N checkmate configurations and then N*M one-move-from-checkmates, and so on. (*Technically it's won/lost/draw.)
The equivalent final state in theorem proving is unique to each theorem so such a system would need to handle an additional layer-of-generalization.
Is this how some of the more advanced chess engines work, or even the not so advanced ones, where there's a point at which it stops searching the forward move tree in greatest depth, and instead starts searching backwards from a handful of plausible (gross move limit-bound) checkmate states looking for an intersection with a shallow forward search state?
The equivalent final state in theorem proving is unique to each theorem so such a system would need to handle an additional layer-of-generalization.