2025.09.21
https://gyazo.com/8868f8df0aa7134ecbcf03a36dea1ef3
執筆中
思った
はやく「何でも許せる方向け」の注意書きを入れてばら撒きたい
まったく初心者の人に論理学入門とLean入門を兼ねる文書を書くことを企画して「論理学がどういう学問なのか」を頑張って書いたのにLeanの入門部分でどう考えても述語論理的なものに触れざるを得なくなって詰みかけてる
普通の数学的議論で形式的な述語論理的なものが意識されているかと言われたらおそらく違うのだけども「「数学の形式化という数学基礎論のモチベーション」の現実的なアプローチ」みたいな感じで定理証明支援系を見るみたいな観点を入れようと企てた結果歪な文書が作られつつある
「数学は形式化できる（数学基礎論の意味で）ということ」を形式化する（定理証明支援系によって）ことで確かめてみましょう
難しい文章書くのダルすぎる．おれの脳の説明が全部出されれば…
メモ
短く出来ないのかなあ
とりあえずこれらの4469とかがどういうグラフなのかわからないので手元で動かしてみるか
観た
めっちゃ良かった．1期よりも更に良くなってる．
すいません 探偵さんが萌えすぎです
メモ
https://nicothumb2img.vercel.app/image/sm43922760#.png https://nico.ms/sm43922760
思った