  We present a method to estimate the provability of a mathematical formula. We
adapt the tactical theorem prover TacticToe to factor in these estimations.
Experiments over the HOL4 library show an increase in the number of theorems
re-proven by TacticToe thanks to this additional guidance. This amelioration in
performance together with concurrent updates to the TacticToe framework lead to
an improved user experience.
