檜山正幸のキマイラ飼育記 (はてなBlog)2026-01-22 型コスモロジー： 型宇宙、型銀河、ユグドラシル 雑記／備忘 最近の証明支援系／プログラミング言語では、通常の型システムの上位に宇宙システム（ソートシステムともいう）を備えたものがあります。2023年の記事「最近の型理論： 宇宙と世界、そして銀河」の冒頭を引用すると： Lean（最新版はLean 4）は強力な型シス… 2026-01-08 「言わないとやらない」の対偶について 雑記／備忘 古典論理では、命題「Pでない ならば Qでない」の対偶である「Q ならば P」は、もとの命題と同値であり意味は変わらないとされます。しかし、対偶命題がもとの命題と同値なことは日常直感と合わない、とも言われます。そのとき出される実例のひとつに「言わ… 2026-01-03 AI支援形式証明への道 報告-4 非専門家と一緒に四苦八苦 雑記／備忘 Lean のコード生成に関しては、GitHu
