カテゴリー: 01-Mathematics

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

計算を止めることが計算の目的である。The purpose of compute is to stop thinking. The goal of computing is the cessation of heuris…
Read more

TANAAKKの研究開発姿勢 TANAAKKのR&Dは、探索の継続ではなく、計算を停止できる構造を発見することを目的とする。 知性とは時間を空間の問題に置き換え、空間の問題を次元の生成原理に置き換えることで計算を…
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）の業績まとめ https://www.math.ias.edu/~lurie 1. 主要著作 「∞-圏論」および「派生代数幾何学」 2. 派生代数幾何学の体系（Derived…
Read more

Higher Inductive Types (HITs) の日本語での定義は、ホモトピー型理論（HoTT）における「型の新しい構成法」として次のように記述されます。 従来の型（データ型）の定義が「値（点）」のみに注目し…
Read more

「Truncatability（切断可能性）」は、高次カテゴリー論やホモトピー理論において非常に専門的な意味を持つ概念です。 一言で言えば、「高次の複雑な構造を、低次のデータだけで完全に復元できるか？」という性質を指しま…
Read more