Mizar

天が落ちてくる心配はやめましょう。みなさん、Mizar（でなくて他の証明検証系でも同じだけど）をかいかぶりすぎ。今のMizarがそのままツールとして普及するはずはありません。そのような未来を心配する必要はありません。

Mizarプロジェクトでわかったことは、「強力な証明検証系があっても、それだけでは使えないね。同じくらい強力な証明編集系を付属させないと駄目だね」です。だったら、証明編集系の研究者の尻を叩けば良い。それだけのことです。それに成功したら、証明の形式化の部分に労力が浪費されることはありません。失敗したら、「結局、証明検証系なんて使えないね」で終るだけです。どっちにしても、数学者にとって不利益はありません。