知乎上有人提问如下：
以下是我的回答：
最早的数学都是从直觉出发的，比如欧几里得就不假思索的使用了“点”、“直线”、“长度”这些概念。
但后来，数学家发现，数学概念只有从一系列确切的公理和定义出发，才能建立起屹立不倒的数学大厦。
尽管欧几里得已经完成了平面几何的公理化，但数学家发现，平面几何中的公理不是本质的，可以从现代数学的公理化出发，自然地涵盖所有平面几何中的内容，题主就注意到了这方面的情况。
恰好，现在有一个方便的数据库，可以查询大部分现代定理的定义内容，这就是Lean Prover的Mathlib。在这个数据库中，我查询到勾股定理的内容是（其实出现了多处，以下是比较简单的一个）：
/-- Pythagorean theorem, if-and-only-if vector inner product form. -/
theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero (x y : F) :
‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0 := by
rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_right_eq_self, mul_eq_zero]
norm_num
把它翻译出来就是：
内积空间中，两个向量, ：
当且仅当.
继续翻译为人话（虽然丢失了一些精确性）就是：
两个向量的模长的平方和等于这两个向量的和平方，当且仅当，这两个向量的内积为0，或称为“正交”，即“垂直”。
这里可以看出，毕达哥拉斯定理就是内积空间中，正交向量的一个普遍性质。
这里看上去出现了很多概念，比如内积空间、向量、模、正交等等，把勾股定理搞得很费解，但这些概念都是有严格定义的，这样才使的数学大厦无懈可击。
这样做的另一个好处是，最大程度的一般化，避免重复造轮子。比如，只要能对向量空间定义出某种合适的“内积”运算，则这个空间中必符合勾股定理，而不必关心这个内积的具体定义。
题主提到的欧几里得空间就是一种内积空间（参考文末关于内积空间的介绍），所以其中自然有勾股定理。
从上述mathlib中的勾股定理定义中，我们看到它还是需要一些证明的，以下这些就是证明步骤：
rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_right_eq_self, mul_eq_zero]
norm_num
所以它仍然是一个定理。虽然根据内积空间的定义，证明勾股定理简直就是一步之遥，但前提是，先有了无数的、确切的概念定义，比如：内积空间、向量、模、正交。所以，感觉上勾股定理在欧几里得空间空间中像是被“定义”出来的。
无论如何，题主的问题非常好，它能帮助我们加深对现代数学的理解。
附：ChatGPT对内积空间的介绍：
内积空间（Inner Product Space）是数学中的一个重要概念，特别在线性代数和函数分析中有广泛应用。它是带有内积（也叫做“点积”或“数量积”）结构的向量空间。这种结构使得我们能够在向量之间定义角度和长度，从而可以推广出很多几何性质，比如正交性和距离等。
定义
设 是一个向量空间，内积是一个映射，它将两个向量 和 关联到一个实数或复数 ，满足以下性质：
对称性（或共轭对称性，如果是复数内积空间）：
对于任意 ，
实数情况下： 复数情况下：，其中 表示复共轭
线性性：
对于任意 和标量 ，
正定性：
对于任意 ，
当且仅当 时，
常见例子
欧几里得空间 ：在这个空间中，向量 和 的内积定义为：这就是我们熟悉的点积。
复数向量空间 ：内积的定义类似，但要注意使用复共轭：
内积空间的几何意义
内积不仅定义了向量的长度（即范数）：还可以用于定义两个向量的夹角，通过内积公式得到：这意味着，当 时，两个向量互相垂直（正交）。
内积空间为研究更复杂的空间（例如希尔伯特空间）打下了基础，它们在量子力学、信号处理和数据分析等领域中也有重要应用。
