>>22
「厳密さは時代の関数」と言った偉い数学者がいたと思ったよ。
完全証明と言うのは、完全に厳密な証明のことであろう。気にスンナ。

>>24
Mizar言語の概要
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch2.htm