東大ロボとかは自然言語で書かれた問題文を内部にもつ形式系に翻訳する技術とか、内部の証明を人間に理解できるよう出力するとか、インプットアウトプットの部分が必要になる。
Coq とか Mizar とかの検証システムは、最初からこの検証システムが処理できる形式的証明を人間が与えてチェックをさせている。人間は普段記号論理で命題を書いても形式的証明なんて理由も無しに書かないし、形式的証明を書くだけでも大仕事。
画像の例は実数の環の理論はすべての命題が真か偽か判定するアルゴリズムがあり、証明も機械的に行えるので、とりあえずそれで解くようにしているという話。
当然AIが苦手とする補助定理を使った証明の方が人間にははるかに簡単な証明となる(現段階では過去の資産を学習した人間と違い、AIは補助定理を見つけるのは大の苦手)。
人間が検証システムを普段から使うようになり、形式的証明のデータベースが集まりAIが[証明]を学習できるようになれば、検証システムではなく自動証明システムの方も実用的なレベルになると思う。まだ先の話だろうけど。