コンピュータは、高度かつ精緻な数学の要求者であると同時に、そのような新しい数学手法の生みの親でもあるのです。即ち、プルーフチェッカーと数学言語の出現を可能にしました。もっと端的に言えばMizarの出現を可能にしたのです。