Machine Learning of Coq Proof Guidance: First Experiments

Cezary Kaliszyk, Lionel Mamane, Josef Urban

We report the results of the first experiments with learning proof dependencies from the formalizations done with the Coq system. We explain the process of obtaining the dependenci…