もしも人間が２０万行も書かなければならないのだとしたら、
実用には耐えられないわな。せめて１千行〜１万行でないと。

＞このプロジェクトの目的は数学の論文のチェックのシステムを作ることです．
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm