ML4PG Introduction:
We present ML4PG, a machinelearning extension for Proof General. It allows to gather proof statistics
related to shapes of goals, sequences of applied tactics, and prooftree structures from the libraries
of interactive higherorder proofs written in Coq and SSReflect. The gathered data is clustered using
the stateoftheart machine learning algorithms available in machinelearning environmnents Matlab
and Weka. ML4PG provides automated interfacing between Proof General and Matlab/Weka. The
results of clustering are used by ML4PG to provide proofhints in the process of interactive proof
development.
Related Projects and Grants:
Related papers (ordered from newer to older):
 J.Heras and E.Komendantskaya, A note on using ML4PG in HoTT (Homotopy Type Theory Library),
and its relation to Dependency graphs.
 J.Heras and E.Komendantskaya, Recycling Proof Patterns in Coq: Case Studies.
Mathematics in Computer Science 8(1): 99116 (2014).

J.Heras, E.Komendantskaya, M.Johansson, and E.Maclean.
ProofPattern Recognition and Lemma
Discovery in ACL2
LPAR'13. LNCS 8312, pp. 389406, 2013.
 J.Heras, E.Komendantskaya ML4PG in Computer Algebra Verification. Systems & Projects session of
CICM 2013. LNCS 7961, pp. 6681, 2013.
Arxiv version.
 E.Komendantskaya, J.Heras. The ARW'13
Workshop abstract Statistical Proof Pattern Recognition: Automated or Interactive? (slides), the 20th Automated Reasoning Workshop (ARW'13), 1112 April 2013.
 E.Komendantskaya, J.Heras and G.Grov. Machine Learning for Proof General: interfacing interfaces.
EPTCS Postproceedings of User Interfaces for Theorem Provers (UITP 2012).
Arxiv version.
Related talks (ordered from newer to older):
Requirements to install ML4PG:
Download
 New version of ML4PG: this version includes all the improvements presented in the paper
Proof Pattern Search in Coq/SSReflect.
 ML4PG Weka version: this version only includes the connection with Weka.
 ML4PG full version: this version includes the connection with Weka and Matlab. You need a Matlab license to run this version of ML4PG.
Installation
After downloading ML4PG, unzip the file and follow the instructions of the user manual.
Code used in different papers:
The code related to the paper Proof Mining with dependent types. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.
The code related to the paper Recycling Proof Patterns in Coq: Case Studies
is available here, and organised by sections. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.
 User scenario 1. ML4PG for Detecting patterns in earlystages of the development.
 User scenario 2. ML4PG for detecting irrelevant libraries.
 The formalisation from the paper "A Constructive Approach to Sequential Nash Equilibria" can be downloaded from the author (R. Vestergaard)
webpage.
 The formalisation from the paper "Acyclicity and finite linear exendability: a formal and constructive equivalence" can be downloaded from the author (S. Le Roux)
webpage.
 The formalisation from the paper "Acyclic preferences and existence of sequential Nash
equilibria: a formal and constructive equivalence" can be downloaded from the author (S. Le Roux) webpage.
 User scenario 3. ML4PG for a teambased development
The code related to the paper ML4PG in Computer Algebra Verification.
is available here. These files can be compiled using Coq v.8.4 and SSReflect v.1.4.
Contact
Please address any queries about ML4PG to katya at computing.dundee.ac.uk