>>280
人間の書く証明は暗黙の了解とか過去の結果の省略とかあり、そのままでは機械的処理ができないので、コンピュータに理解できる形式化された証明に書き直す必要がある。
慣れた数学者なら大学の教科書一頁を数日で形式化完了という話だったと思うから、ものすごい大変な作業が必要。
形式化さえできれば、証明の正しさの検証をコンピュータは確実に処理してくれる。人間が匙を投げた証明を形式化し直して検証システムで正しいと示した例は既にある。
その検証システム自体が正しく機能しているかは、そのプログラムを人間が見て正しいと信頼するしか無いんだけどね。ある検証システムは高々400行程度で書かれているそうで、まあ大丈夫と信じられている。
これとは別の話になるが、今年、人間が一生かけて記憶できるデータ量をはるかに超えるデータを用いて予想の反例をコンピュータで見つけたというニュースがあった。今後数学においても人間の検証を諦めてコンピュータを信頼することは避けられないと思われる。