Mizar

2005年に信州大工学部教授の中村八束氏らが
Jordan曲線定理(「閉じた曲線が平面を、内と外とに分ける」という
直感的には明らかな定理)の
(厳密な最終)証明( ftp://mizar.uwb.edu.pl/pub/fm/jordan.pdf )を検証するのに使用した
プルーフ・チェッカー・ソフトウェア(非商用利用に限りフリーの)。
論文として利用できることを目指しており、Mizarで記述された証明文はそのままで
可読性があるように開発されている。

http://ja.wikipedia.org/wiki/Mizar
http://markun.cs.shinshu-u.ac.jp/...
http://mizar.org/