形式的証明と非形式的証明
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/12/16 07:47 UTC 版)
数学で日常的に行われている「非形式的」証明は、証明論で言う「形式的」証明とは異なる。しかしながら、それは形式的証明の高度に抽象化されたスケッチのようなもので、専門家が十分な時間と忍耐を持っていれば、非形式的証明から形式的証明を適切に再構築できるようなものである場合が多い。比喩的に言えば、そのような場合に完全な形式的証明を書くことは、機械語でプログラミングをするようなものである。 現代では、形式的証明は一般に計算機支援証明を補助としてコンピュータを使って構築される。また、その証明がコンピュータで自動的に検証される点も重要である。形式的証明の検証は簡単だが、証明そのものをコンピュータが構築すること（自動定理証明）は一般には非常に困難である。一方、数学における非形式的証明は査読による検証に何週間も要し、それでもまだ誤りが含まれていることが多い。
※この「形式的証明と非形式的証明」の解説は、「証明論」の解説の一部です。
「形式的証明と非形式的証明」を含む「証明論」の記事については、「証明論」の概要を参照ください。
ウィキペディア小見出し辞書の「形式的証明と非形式的証明」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 形式的証明と非形式的証明のページへのリンク
