A proof system for graph (non)-isomorphism verification

TL;DR

This paper develops a formal proof system for graph canonical labelling algorithms, enabling independent verification of graph isomorphism checks in theorem provers.

Contribution

It formalizes a state-of-the-art graph canonical labelling algorithm within a proof system and provides an implementation for generating verifiable proofs.

Findings

Proofs can be independently verified to confirm graph non-isomorphism.

The formalization ensures correctness and trustworthiness of graph isomorphism results.

Implementation supports integration with interactive theorem provers.

Abstract

In order to apply canonical labelling of graphs and isomorphism checking in interactive theorem provers, these checking algorithms must either be mechanically verified or their results must be verifiable by independent checkers. We analyze a state-of-the-art algorithm for canonical labelling of graphs (described by McKay and Piperno) and formulate it in terms of a formal proof system. We provide an implementation that can export a proof that the obtained graph is the canonical form of a given graph. Such proofs are then verified by our independent checker and can be used to confirm that two given graphs are not isomorphic.