2026.07.11

https://gyazo.com/1cc4d52ee237640b9e292a017206e490

観た

思った

とりとめないメモ

今後の過渡期、まだAIと人間ががんばって協働する時代において、AIがよこしてきた大量の形式証明を読むにあたってそれがちゃんと人間に読みやすい"表示"であることは重要だと思う、つまり定理証明支援系のためのフォント制作は自己満足以上にかなりの実利があるのですよという正当化が出来るのでは。

10年ぐらいダブステップ・キッズなのにSkrillex - All Is Fair in Love and Brostep w/ Ragga Twinsの歌詞ちゃんと見たことないなと思って調べた

例えば自然数の1が存在しそうということはリンゴを適当に1個もってこれば正当化できそうだが、2^2^2^1000という自然数が存在することを正当化することは難しい、この宇宙が適当な不可分な物体をその数集めたら突然何の理由もなく消滅しないということはまだ保証されていないはず