畢達哥拉斯定理

數學敘述

在歐幾里得平面中的任一直角三角形，若兩股長為 a、b，斜邊長為 c，則 a 的平方加 b 的平方等於 c 的平方。

代表公式（精確 TeX）

a^2+b^2=c^2

成立條件

• 幾何背景為歐幾里得平面。
• 三角形具有一個直角。
• a 與 b 表示兩股長，c 表示斜邊長。
• 邊長為非負實數。

符號作用域

• a — 第一股長
• b — 第二股長
• c — 斜邊長

直觀、定義與常見誤解

這個定理不是對所有三角形成立，而是針對直角三角形。斜邊是直角所對的最長邊。

平方和可以視為以三條邊為邊長所建立的正方形面積關係：兩個股上正方形的面積總和，等於斜邊上正方形的面積。

程式可以檢查具體的數值三元組，也可以搜尋整數畢氏三元組；但有限檢查不能取代定理的普遍證明。

Lean／Mathlib 先證明向量夾角版本，再由 IsRightTriangleSideModel 明示綁定 a=‖x‖、b=‖y‖、c=‖x+y‖，推出中文條目使用的 a²+b²=c²。

把 a²+b²=c² 套用到任意三角形，或把已形式化的指定向量邊長模型誤認為所有仿射表示法都已自動完成等價證明。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 直角三角形 — 定理的適用對象。
• 歐幾里得長度 — 平方關係依賴歐幾里得距離。

驗證界線

Python 與 FELRA 提供有限計算證據；Lean／Mathlib 分別證明向量核心及 OCME 宣告的邊長綁定模型。任意仿射三角形表示到此模型的等價仍需另外證明。

formalized_declared_side_model

• evidence-sha256-49083d0529f2b530b946fd6f30a313b0341a8989bf0f6de9adcdeb398a2b4466
• evidence-sha256-97ad4a4b529de8c77662f823ad0966c24cfe1c121af8cbb4320135b9ea849448
• evidence-sha256-4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752
• evidence-sha256-701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e

下一個義務

建立任意歐幾里得仿射三角形頂點表示與 IsRightTriangleSideModel 的等價定理，包含頂點排列、邊向量方向與距離保存。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。