那个链接的作者及讨论者不懂得定理的机器证明。
有Tarski–Seidenberg theorem 和 Quantifier elimination（https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers）之后平面几何的机器几何定理的机器证明在理论乃至算法上没大的意义。Wu算法和buchburger 算法（http://www.scholarpedia.org/article/Buchberger%27s_algorithm）大约都超出了平面几何而且相近，算法复杂度太高，只在一个退缩或小规模的情况下实用。

老实讲，没仔细看Wu的算法。
【 在 b0207191 的大作中提到: 】
: 吴文俊做的成果有没有实用化，比如初中平几证明题，有没有工具可以输入条件后自动输出证明过程
: 网上搜索发现还有异议的
: https://bbs.pinggu.org/forum.php?mod=viewthread&tid=5579005&pid=44003068&page=1
: ...................
--
FROM 183.228.218.*