形式化された公理系の上に構築された数学は
機械的な操作によって定理は証明される。
人の脳が万能機械の域をでないものならば、
天才が証明できる数学の定理は機械にも証明できる。