此帖转自 forecasting 在 STEM 的帖子：Re: 还AI拥有顶级数学家能力？？我给它5条公理，它能无中生有的 把所有平面几何定理推导出来吗？
Tarski实闭域判定算法（Real Closed Fields, RCF）的应用之一就是证明欧式几何的所有定理。
Tarski 实闭域的判定算法，本质上就是一阶实数理论（First-order Theory of Real Closed Fields）的量词消去（Quantifier Elimination）。它的复杂度经历了几十年的改进。
事实上，RCF 因为具有量词消去和 o-minimal 结构，其可定义集合始终是半代数集，这也是其复杂度与 Presburger 算术、代数闭域判定之间形成明显对比的原因。
平面几何的情况有中科院院士张景中做的系统，理论意义几乎没意义，但可用于教育，可没推广开。
吴文俊那套算法跟Tarski差不多，所以理论意义也不大
@TheMatrix 多奖赏一些分，我难得愿意写这么多，而且质量不错
