Non-surveyable proof とは

数学の哲学では、非調査可能な証明は、人間の数学者が検証して論争の妥当性を証明するのは実行不可能と考えられる数学的証明である。この用語は、1980年にトーマス・ティモチコによって、4色定理のコンピュータ支援の証明であるケネス・アペル(Kenneth Appel)とヴォルフガング・ホーケン(Wolfgang Hakenen)の批判で造語され、それ以来、過度の格の分割や派遣された検証が困難なコンピュータプログラムです。測量能力は計算上の数学において重要な考慮事項です。