>>284
＞別に「形式的証明」がなくても不安じゃありませんけど。

ごもっとも。
数学の証明はプログラム検証とは違う。
数学は読んだ人が理解できればそれでよい。
ギャップは読者にとって自明でないから問題になるのであって
多くの専門家が「自明」と判断すればそれはギャップでなくなる。

「玄人の誤解」とは、数学が実は数学者の頭の中の世界における
共同の了解事項であるにすぎないにもかかわらず、あたかも
自分たちとは全く独立なる真偽の根拠があると信じていること。
そしてそれが嘘であることを暴くのが形式的証明。
なぜなら、誰一人了解しない機械的検証を、数学者はまったく
信頼しないからである。