AB=BC，I为ΔABC内心，BM=MI，AP=3PC，H在PI上，MH⊥PH，Q为外接AB弧中点，证：QH⊥BH

天山草@

机器证明的最高目标，应计算出上图所有点的位置坐标，然后搜索哪些点是三点共线？哪些点是四点共圆？哪些线是平行的？哪些线是垂直的？哪些线段是长度相等的？哪些角度是相等的？哪些三角形是全等的？哪些三角形是相似的？哪些图形是面积相等的？哪些是线段乘积相等的？哪些是点到线段距离相等的？等等。
      当然，这些信息中，大多数应该是无用的。但是，一旦有什么新发现，就可能产生一个新的几何定理。
      这个国内外的学者都在研究。目前还没有公开发布的成熟软件。

天山草@

下图是国内某学者的成果。来源：数学研发网站。

denglongshan

注意红色标记的结论

天山草@

机器证明的发展趋势，我的理解是要完成三件事，一是巧妙的构图，二是解出所有点的坐标，三是对所有点进行搜索检测，看看哪些线段相互平行、垂直、相等，哪些三角形相似、全等，有几处三点共线、四点共圆，等等等待。
这三件事情，最困难的是第二件。如果构图不当，有可能求不出点位置坐标的解析式。另外，似乎用复数法求解点的位置对于 mathematica 来说，比用实数横坐标和实数纵坐标方案要困难许多。这可能是因为 mathematica 目前对复数运算还远不如对实数运算来得完善。这也许是学术界有人不接受共轭比概念的一个原因？ 以共轭比方式来表达点的复数位置，公式会显得比较简捷美观，但是往往在求解复数方程时会死机，或者说长时间算不出来。

王守恩

天山草@ 发表于 2020-12-19 12:19
机器证明的最高目标，应计算出上图所有点的位置坐标，然后搜索哪些点是三点共线？哪些点是四点共圆？哪 ...

利用11楼的图。
若 BI 垂直 QM，BQHM 四点共圆，则
∠MHB+∠HQM+HMQ=∠MHB+∠HBM+∠HIM=∠HMI+∠HIM=90

denglongshan

对于线性构造，算出点对应的表达式容易，而对于非线性，则很困难，比如求内心表达式，果先构造三点，用直线方程求解很难。

denglongshan

天山草@ 发表于 2020-12-20 12:31
机器证明的发展趋势，我的理解是要完成三件事，一是巧妙的构图，二是解出所有点的坐标，三是对所有点进行搜 ...

构图很重要，对简化计算有很大作用，你看看这片帖子。
https://bbs.emath.ac.cn/forum.php?mod=viewthread&tid=17639&pid=87369&page=1&extra=#pid87369