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

翻译：为了能够在交互式理论验证中应用图形异形检查,必须机械地验证图形异形检验算法,或者其结果必须由独立的检查员核实。我们分析一个最新水平的图形异形检查算法(由McKay和Piperno描述),并以正式的验证系统的形式将其制成。我们提供了一个执行程序,可以导出一个证据,证明获得的图形是某一图的典型形式。这些证据随后由我们的独立检查员核实,并用来证明两个给定的图表是非异形的。