形式的証明に拘ってる一名は放っておいてプルーフチェッカーについて話そうぜ

とりあえず http://mizar.org/fm/ と20万行目に目を通したんだけど，ほとんど全てが
定式化のための定式化で冗長としか思えんかった．
知識蓄積する以外になんかこのあたり簡単にできんかな？