Computing Persistent Homology within Coq/SSReflect

TL;DR

This paper presents a formalized approach to computing persistent Betti numbers, a key component of persistent homology, using the Coq proof assistant, demonstrating the maturity of theorem provers for complex mathematical formalization.

Contribution

It introduces a formal development of certified algorithms for persistent Betti numbers within Coq/SSReflect, formalizing the underlying mathematical theory.

Findings

Successful formalization of persistent Betti numbers algorithms

Demonstrates theorem prover maturity for complex mathematical theories

Provides certified computational tools for topological data analysis

Abstract

Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.