I have not fully read the whole page, but I wonder if this type of tree of expressions leading to a proof can be explored efficiently with the same idea as Mont

I have not fully read the whole page, but I wonder if this type of tree of expressions leading to a proof can be explored efficiently with the same idea as Monte-Carlo Tree Search in chess. I.e. surely you can explore all the possible combinations of existing axioms/lemmas, but if you have something like NN, it can suggest the most interested branches of the tree, so you can go deeper in the tree/graph without exponential effort.