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.

翻译：为了在交互式定理证明器中应用图的规范标记和同构检查，这些检查算法必须要么经过机械验证，要么其结果能够由独立的检查器验证。我们分析了一种最先进的图规范标记算法（由McKay和Piperno描述），并将其形式化为一个形式证明系统。我们提供了一个实现，能够导出证明，表明所得到的图是给定图的规范形式。此类证明随后由我们的独立检查器验证，并可用于确认两个给定图不是同构的。