自動証明なんて出来ないから考えてもムダ。
それより、表題の件は証明チェッカーを通すために人間が
証明を機械にわかる形に書いたのが２０万行ってことだろうな。
このステップ数をなんとか数千行くらいまで落とせれば実用になるだろう。