カテゴリー: Logic

ルーリー（Lurie）のいう infinitude（無限性） と、ヴォエヴォドスキーの Univalent Foundations（一価性基礎付け） を結びつける背景は「局所（Local）から全域（Global）への無限…
Read more

IAS（プリンストン高等研究所）の物理学、特に弦理論（String Theory）や量子重力、ホログラフィー原理（AdS/CFT）を研究している層において、ヴォエヴォドスキーやルーリーの数学的基盤が「OS」のように機能し…
Read more

“真に意味のある同一視は、要素の完全一致（strict equality）ではなく、構造保存的な可逆性＝equivalence によって与えられる” 論点は、 なぜ Voevodsky や Lurie のように、stri…
Read more

Teleological Finity Bypassing とは、特定の**「目的（Telos）」を最終的な「同一性（Identity）」としてInvariants化し、そこに至るまでの膨大な「有限のステップ（Finit…
Read more

エミー・ネーター（Emmy Noether）の功績は大きく分けて2つの柱があります。1つは物理学の根幹を成す「ネーターの定理」、もう1つは現代数学の景色を塗り替えた「抽象代数学(abstract algebra)」の確立…
Read more

証明アシスタントとライブラリの対応表 証明アシスタント (Tool / Language) 主要な数学ライブラリ (Library) 特徴 Coq UniMath / Mathematical Components Un…
Read more

Coq（現在のRocq）の歴史は、ChatGPTやGeminiといった現代の生成AIが登場するよりも遥かに長く、深いものです。 1. Coq Coqの開発が始まったのは1984年。フランスのINRIA（国立情報学自動制御…
Read more

UniMath 通常の数学者が紙とペンで書く「定理と証明」が、Coqの世界ではどのように「型（Type）」と「項（Term）」に置き換わるのか。 1. 「証明」という名のプログラム コードは関数型プログラミング（Hask…
Read more

ウラジーミル・ヴォエヴォドスキー（Vladimir Voevodsky）の業績、「代数的K-理論・モチヴィック・コホモロジー」「ホモトピー型理論（HoTT）・単価基礎（Univalent Foundations）」 ウラ…
Read more

ジェイコブ・ルーリー（Jacob Lurie）の業績まとめ 1. 決定版：主要著作（Monographs） 「∞-圏論」および「派生代数幾何学」 2. 派生代数幾何学の体系（Derived Algebraic Geome…
Read more