正しさの確認と言えば、つまりは、自分が使う定理は全て、ZFC からの証明図が書けることを検証しろと言うことなんだよね。