証明を書き下すのが手間なのもあるが、数学のオブジェクトをプログラムで扱えるよう定義するのも相当手間だろうね

行列式→行列式を計算するのは簡単だが、置換を使って定義するのはめんどくさそう。置換群を先に定義しなければならない

リーマン積分→区間幅の最大値が0に収束するようなリーマン和の列すべてを考えなければいけない。

商空間で辺に沿って同一視した曲面とかもめんどくさそう。