証明オブジェクトとしてのラムダ項

• Title: A comparison of the mathematical proof languages Mizar and Isar
• Markus Wenzel, Freek Wiedijk
• Pages: 24p
• URL: http://www4.in.tum.de/~wenzelm/papers/romantic.pdf

P.24からの引用（画面ショット）

証明している定理は：

• for every number n there exists a prime p > n

論文の著者は：

• マルコス・マカーリオス・ウェンツゥ ：本編ではウェンツェルと書いていたが、forvoでの発音はウェンツゥに聞こえる。マカーリオス（Makarius）は宗教上の名前だと思う。
• フリーク・ウェダイク ：可読な証明にするためにMizar Modeを色々と実装している。Mizarに詳しく、タクティク言語も書けるプルーフハッカー。