基本的な質問で申し訳ありませんが、任意の数学の定理の証明は
その証明が正しいならばコンピューターが理解できる形の形式的な証明に書き直せますよね？