TPPmark2014 http://imi.kyushu-u.ac.jp/lasm/tpp2014/tppmark2014-2.pdf の問題、今回は割とシンプルな数論的な問題なのね。 インフォーマルな証明はできたが、これをちゃんと形式化するのは結構大変そうだなぁ。