  We study Monte Carlo Tree Search to guide proof search in tableau calculi.
This includes proposing a number of proof-state evaluation heuristics, some of
which are learnt from previous proofs. We present an implementation based on
the leanCoP prover. The system is trained and evaluated on a large suite of
related problems coming from the Mizar proof assistant, showing that it is
capable to find new and different proofs.
