2026.07.19
https://gyazo.com/9e7a398b690d340ece70aa7c5e35d429
観た
ギャオーーーーン
メモ
あまり定理証明支援系とは縁がない人と話して，結構向こう側から新鮮に驚かれたこととして： 例えば無限的な構造，あるいは，計算できないようなものが，コンピュータプログラムとして定義出来たり，証明できたりすることが可能という点にかなりびっくりしていた．
つまり究極的には項書き換え系なのでそういうことが出来るんですよーみたいなふわっとした説明で済ませたのだけど，もしかしたら純粋に数学屋の人は定理証明支援系について，このような先入観があって，定理証明支援系に力を小さい方向に見積もっている可能性もあるのかもしれない．．． 我々がやることは，実は大きな定理をちゃんと検証しました！ということではなくて，普通の数学的な議論がある程度普通に?出来ることを強調・デモンストレーションしていくことなのかもしれない．．．
思った
ひたすらリファクタリング．
$ \mathbf{PA}^\omegaなにーーーーー；；