投稿者: TANAAKK

現代物理学は数学的定理により発見された空間生成原理のスキーマおよび、幾何代数的な空間上の粒子運動法則と、実数空間による抵抗力の誤差を特定する学問領域です。「幾何代数的な理想の法則」と「実数空間の複雑な誤差」の間に、AIと…
Read more

アルカニ＝ハメド教授やマルダセナ教授、ウィッテン教授たちが、それぞれの理論（ADDモデル、M理論、アンプリチュードヘドロン）において、その存在を予言・前提としている**「未発見の粒子」**には、いくつかの重要な呼び名があ…
Read more

1. 最大の功績：AdS/CFT対応 1997年にフアン・マルダセナが発表したこの理論は、現代物理学で最も引用される論文の一つです。 2. 「ER = EPR」：ワームホールと量子もつれ 近年、マルダセナが提唱したアイデ…
Read more

1. 「重力はミリ単位」（大きな余剰次元） ニマ・アルカニ＝ハメド教授は、1998年にサバス・ディモポロス、ギア・ドヴァリと共に 「ADDモデル（大きな余剰次元理論）」 を提唱しました。 2. 「HoTT（ホモトピー型理…
Read more

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

三大数学的証明ツールの比較図解 ツール 出自・歴史 核心的な思想 Cursorでの使用 Coq / UniMath 1984年〜（仏 INRIA）ヴォエヴォドスキーが中興 「構造の厳密さ」数学をプログラム（型）と見なす。…
Read more

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

TANAAKKでは事業を数学、自然科学の公式を用いて組み立てようとしており、結果としては純資産2倍を12年間続けてきたものの、戦いの規模が数十億円に達すると、一つの致命的な間違いが全体を揺るがすことになってしまうという懸…
Read more

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

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