Statistical Proof Pattern Recognition: Automated or Interactive?

TL;DR

This paper compares various approaches used in data mining of large proof libraries within automated and interactive theorem proving to evaluate their effectiveness.

Contribution

It provides a comparative analysis of existing methods for proof pattern recognition in theorem proving environments.

Findings

Identifies strengths and weaknesses of different approaches

Highlights the most effective techniques for proof pattern recognition

Suggests directions for future research in automated theorem proving

Abstract

In this paper, we compare different existing approaches employed in data mining of big proof libraries in automated and interactive theorem proving.