ML4PG in Computer Algebra Verification

Jonathan Heras, Ekaterina Komendantskaya

Research output: Chapter in Book/Report/Conference proceedingChapter

7 Citations (Scopus)


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 languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationMKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings
EditorsJacques Carette, David Aspinall, Christoph Lange, Petr Sojka, Wolfgang Windsteiger
Number of pages5
ISBN (Electronic)9783642393204
ISBN (Print)9783642393198
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


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


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

Cite this