I don't know about theorem provers but computational algebra systems work a bit like a blockhain. At least they both use a merkle tree to store their graph/tree

I don't know about theorem provers but computational algebra systems work a bit like a blockhain. At least they both use a merkle tree to store their graph/tree/list, but somewhere in your description there is a reformulation of the halting problem. It is impossible to know what rule is going to be useful next, CAS systems will often just use the length of the expression to decide this order. Like knuth said once, maybe P=NP but P is just impractically big.