耳鼻科に行きました
教員が数学の実績主義の風潮にぼやいていて、自分も実績主義に飲み込まれてしまっているなあと思った
2 時には寝る系 VTuber、虹庭ネル
GPT-5 は質問に応じて Thinking が入ったり入らなかったりするから、Thinking が入ると、AI をちゃんと考えさせる質問ができたという気分になってちょっと嬉しくなる
あっ情報ありがとうございます、とりあえず資格情報 PDF を画像に変換を……
えー、Web 問診で健康保険証の資格確認書の画像を求められたんだけど……そんなのどっかやってしまった……
みんな基礎に興味ないというのは、foundations-free な部分だけに興味があるってことで、それはまさに synthetic mathematics がやりたいことだと思うんだけど
Lean がこれだけ使われてて、Grothendieck 宇宙もみんな仮定する中で、もはや「誰もが ZFC で考えている」とは言い難いと思うんだけど、set-level type theory ではあると思うんだよなあ。でも Lean にだいたい翻訳できてる時点で「誰もが集合論で考えている」とも言えないのかなあ。
記号の形式的操作に還元するという基礎の問題と、集合論 vs 型理論みたいなのって、おそらくかなり別の問題なんだけど、きっぱりとした境界はないので、「ZFC 集合論の問題」というといろいろ一緒くたになってしまう感じはある
「foundations の話をしない方がウケがいいのでは」と言われているのを見るとちょっと悲しくなるけれど、そういう話をきちんとするのは難しいというのもわかる
