AD是△ABC的角平分线，AD交外接圆于E，DF⊥AC交圆于F，AN⊥BF交BC于N，证EFN共线。，

天山草

经过 D 点与 AC 垂直的直线与圆的交点有两个，即 F 和 F1。因此出现两种不同的图形，每一种都符合三点共线的要求。

天山草

cgl_74

这就是所谓的计算机证明吗？
有问题咨询下：
一、既然是计算机证明，是否很多模块函数都已经固定化了？就像API函数一样，几乎不用额外编程。
举例：由图形构造上看，题目给定了三角形ABC的顶点坐标，那么题目中所有点都已经确定了。比如角平分线，外接圆等。是否计算机就能智能的算出各种点，线的坐标或方程。
那么结论中的是否共线的判断，就很明显且简单了。
二、我的意思是，如果计算机能做到这个程度，那这种几何题就非常简单了。由图形构造的因果关系，看目标的点的坐标，或线的方程，圆的方程，很简单就能判断结论是否成立。
如果居然计算机还不能这样做，这就是你工作努力的方向。既然都用到计算机了，还需要这样去编程吗。。。。。

天山草

答复  cgl_74：
对于某种常用的构图，其常见的坐标点事先都已算出了，可作为现成公式引用。但是你不可能对千百种可能的点全都算出来现成的公式放在那里供调用。所以对于不同的问题，都需要编程计算。而是由人工编程，还是由人工智能编程，那就是另一个问题了。人工编程当然是低级阶段，是我们这些数学爱好者娱乐的小玩意儿。专业的计算机证明跟这个还是有区别的。
要强调的是，中学生不宜学习这些非教学大纲要求的东西，因为考试只考纯几何证明和某些传统的解析几何证明。中学生学习这些东西纯粹是浪费时间和精力。