### Abstract

ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library - a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.

Original language | English |
---|---|

Title of host publication | Intelligent Computer Mathematics |

Subtitle of host publication | MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings |

Editors | Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger |

Publisher | Springer |

Pages | 354-358 |

Number of pages | 5 |

ISBN (Electronic) | 9783642393204 |

ISBN (Print) | 9783642393198 |

DOIs | |

Publication status | Published - 2013 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 7961 |

ISSN (Print) | 0302-9743 |

### Keywords

- ML4PG
- Interactive Theorem Proving
- Coq
- SSReflect
- Machine Learning
- Clustering
- CoqEAL

## Fingerprint Dive into the research topics of 'ML4PG in Computer Algebra Verification'. Together they form a unique fingerprint.

## Cite this

Heras, J., & Komendantskaya, E. (2013). ML4PG in Computer Algebra Verification. In J. Carette, D. Aspinall, C. Lange, P. Sojka, & W. Windsteiger (Eds.),

*Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings*(pp. 354-358). (Lecture Notes in Computer Science; Vol. 7961). Springer. https://doi.org/10.1007/978-3-642-39320-4_28