形式化資料專區
本頁導覽
- 公開 OCME 實際使用的 Lean 原始碼。
- 形式證據目錄
- mko-tends-to-relation
- 限制與未涵蓋範圍
- mko-euclid-pythagorean-theorem
- 限制與未涵蓋範圍
- mko-euclid-pythagorean-theorem
- 限制與未涵蓋範圍
- mko-set-membership
- 限制與未涵蓋範圍
- mko-function-mapping
- 限制與未涵蓋範圍
Lean 核心接受一個 proof term，不代表百科全文、自然語言語義橋或所有等價幾何表示都已自動證明。這裡同時公開通過項目與尚未封閉的邊界。
公開 OCME 實際使用的 Lean 原始碼。
公開內容包含 OCME 自有 Lean 原始碼、固定工具鏈、Lake 專案設定與 dependency lock；不包含 .lake、已下載的 Mathlib 原始碼、套件或編譯快取。重播時由 Lake 依 lock file 取得依賴。
查看 SHA-256 manifest
形式證據目錄
mko-tends-to-relation
對任意函數 f:α→β 與濾子 l₁、l₂，Filter.Tendsto f l₁ l₂ 與 Filter.map f l₁≤l₂ 等價。
evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d · passed
限制與未涵蓋範圍
- 此證據形式化 Mathlib 的濾子趨近語義；裸符號 x→a 必須先指定來源與目標濾子才能連到此聲明。
- 它不是單獨的 ε–δ 極限定義，也不直接證明任何特定函數極限。
- 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。
查看原始 Evidence JSONmko-euclid-pythagorean-theorem
在任意實內積空間中，若向量 x 與 y 的夾角為 π/2，則向量和的範數平方等於兩向量範數平方之和。
evidence-sha256-4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752 · passed
限制與未涵蓋範圍
- 此證據證明向量核心定理；邊長角色的明示綁定由獨立的 pythagorean_side_lengths 證據承擔。
- 本證據依賴 Lean 4.30.0 核心、Mathlib v4.30.0 與指定匯入模組。
- 形式證明不取代中文敘述、符號角色與幾何模型的人工審查。
查看原始 Evidence JSONmko-euclid-pythagorean-theorem
對任意實內積空間、向量 x、y 與實數 a、b、c，若 x、y 夾角為 π/2，且 a=‖x‖、b=‖y‖、c=‖x+y‖，則 a·a+b·b=c·c。
evidence-sha256-701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e · passed
限制與未涵蓋範圍
- 此證據完成 OCME 宣告之向量邊長模型；它不自動等同於所有仿射平面、座標系或三角形建構方式。
- 模型中的斜邊長被定義為向量和的範數；其他頂點排列需另證與此模型等價。
- 本證據依賴 Lean 4.30.0、Mathlib v4.30.0 與 pythagorean_vector。
查看原始 Evidence JSONmko-set-membership
對任意型別 α、元素 x:α 與集合 A:Set α，命題 x∈A 與謂詞求值 A x 等價。
evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d · passed
限制與未涵蓋範圍
- 此證據形式化 Lean Set 作為 α→Prop 的集合語義，不宣稱涵蓋所有集合論基礎系統。
- 程式容器的成員測試仍不會因此自動等同於一般數學集合隸屬。
- 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。
查看原始 Evidence JSONmko-function-mapping
對任意型別 X、Y、函數 f:X→Y 與輸入 x:X，存在唯一 y:Y 滿足 f x=y。
evidence-sha256-d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b · passed
限制與未涵蓋範圍
- 此證據形式化 Lean 總函數型別的存在唯一輸出語義，不涵蓋部分函數、隨機程序或有副作用程式。
- 陪域 Y 與函數實際值域仍是不同概念；本定理不聲稱 f 為滿射。
- 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。
查看原始 Evidence JSON