■

有名な数学の定理100個を様々な証明支援系で形式化している
http://www.cs.ru.nl/~freek/100/
ProofPowerというのは初耳だけど、Coq , Isabelle , Mizarあたりは、どれも30個程度しか形式化できていないのに対して、HOL Lightだけが60個以上と飛びぬけている。Mizarなんかは、数学に特化しているイメージがあったのだけど、意外とそうでもないのか。にしても、この差はユーザの数の差なのか、機能の差なのかというのは気になる