■

A modular formalisation of finite group theory
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.5995
という論文を眺めたりした。CoqとCoqのライブラリであるSSReflectを使って、Feit-Thompsonの定理の証明を形式化しようという話らしい。試みとしては面白いけど、研究としてはどうなんだろうっていう。まあ、頑張ればきっと書けるのは書けるんだろうし(とてもしんどいとは思うけど)。

こういうのは、Wikipediaみたいに、ヒマ人がちょこちょこCoqのコードを投げていくと、そのうち証明が完成するというスタイルがいいんじゃないかとか思ったりもした。Wikipediaスタイルで、有志で完全にformalな数学辞典を作るとかは結構面白い気がする。名前は、Bourbakipediaとかで(

しかし、有限単純群の分類定理とか、数百年後には、ニュートンの平面三次曲線の分類みたいな扱いになってそうだな。