>>77
やっぱleanによる形式化って
全数学を基礎から検証するようなものじゃなくて
ある程度の共通認識をブラックボックス化して
そこから形式的に導けるかだけ検証するってことか
これまでのライブラリってのも
全部そういうものなのかな？