数学的厳密性
確かに、コンピューターの助けを借りて、いくつかの証拠を機械的にチェックすることが可能である 。形式的厳密性とは、形式言語による高度な完全性の導入であり、 ZFCなどの集合論を使用してそのような証明を体系化できる(自動定理証明を参照)。
公開されている数学的議論は厳密さの基準に準拠している必要があるが、象徴的な言語と自然言語の混合で書かれている。この意味で、書かれた数学的記述は形式的な証明のプロトタイプである。多くの場合、書面による証明は、まだ正式化されていない可能性がある、厳密なものとして受け入れられる。数学者が非公式に書くためにしばしば引用する理由は、完全に正式な証明はより長く扱いにくい傾向があり、それによって議論の線が曖昧になるためである。人間の直感に明白に見える議論は、実際には公理からかなり長い形式的な導出を必要とするかもしれない。特によく知られている例を、ホワイトヘッドとラッセルが、プリンキピア・マテマティカで「1 + 1 = 2」について示している。要するに、書面による記述では、形式よりも理解しやすさが優先される。
それでも、自動定理証明の支持者は、証明の形式化は、非公式の書面による談話のギャップや欠陥を開示することによって、数学的な厳密さを改善すると主張するかもしれない。証明の正しさが争われる場合、形式化は、誤解やあいまいさを減らすのに役立つため、そのような論争を解決する方法である。