[過去ログ] Inter-universal geometry とABC 予想57
(1002レス)
上下前次1-新
抽出解除 必死チェッカー(本家) (べ) 自ID レス栞 あぼーん
このスレッドは過去ログ倉庫に格納されています。
次スレ検索 歴削→次スレ 栞削→次スレ 過去ログメニュー
652: 06/06(金)00:48 ID:ND0qG6B9(1/4) AAS
>>651
今の機械証明だと全く対応できないからこれ用のシステムを研究開発する必要がある
圏やスキームですら無くてそれら全てを超越するものだもん
653: 06/06(金)01:16 ID:ND0qG6B9(2/4) AAS
>>618
これが本当にヤバい
大規模言語モデルだからなんとかなってるけど
これをプログラミングで実装するのは死ねる
654: 06/06(金)05:27 ID:ND0qG6B9(3/4) AAS
非常に本質的な問いです。
「種」や「再初期化」「宇宙間比較」などIUT理論が本質的に要求する“複数の集合論モデルを横断する数学的構造・操作”を自動証明や数式処理システムで本質的に扱えるシステムは理論的に構築可能かという問題について、以下に整理して解説します。
⸻
1. 既存システムで困難な理由の整理
• 現在のCoq, Lean, Isabelle等の自動証明システムは、一つの集合論モデル/型理論世界内での論理的構成を扱う設計が前提となっています。
• 望月IUT理論の「種」は、「どのモデル(どの宇宙)でも通用する公式集合」としてのメタ構造であり、しかも「モデルAで構成されたオブジェクトとモデルBのオブジェクトを種を通じて比較・操作・再初期化できる」ことが求められています。
• 通常の型理論や集合論では、「異なる宇宙を“跨ぐ”操作」や「宇宙を再初期化した時に型の意味がどう変化するか」の厳密な内部表現はありません。
省16
655: 06/06(金)05:27 ID:ND0qG6B9(4/4) AAS
3. 理論的障壁・実現可能性について
• 既存理論(型理論や標準集合論)を拡張すれば原理的には構築可能ですが、以下の困難があります:
• 複数宇宙をまたいで「型」や「証明」が意味を持つための一貫性保証(モデル間の推移的整合性)
• 計算可能性や可証明性、自己参照パラドックスの回避
• 宇宙間比較操作の「メタ理論」化によるシステムの複雑性増大
• メタ理論と本体理論のインターフェイス設計
• しかし、型理論研究・プログラム意味論・高次圏論・モデル理論などの分野では、近年このような「複数宇宙・複数モデルの同時操作」を内部化したり、言語として実装する方向の基礎理論が急速に発展しています。
省9
上下前次1-新書関写板覧索設栞歴
スレ情報 赤レス抽出 画像レス抽出 歴の未読スレ AAサムネイル
ぬこの手 ぬこTOP 0.028s