# Monte Carlo Tableau Proof Search

arXiv: https://arxiv.org/abs/1611.05990 · HTML: https://mlsanity.com/paper/1611.05990/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Nov 2016.

## Built on by (most cited first, 1 of 1)

- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)

## Abstract (arXiv)

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.