一条很难用公理证明的几何新定理？
这条几何定理点击超万次，还没有其它证明方法。Fb是Feuerbach点（三角形的九点圆与内切圆或旁切圆的切点），试证明：Fb关于三边切点构成的三角形DEF，三个中点构成的三角形MaMbMc，三个垂足HaHbHc构成的三角形的Simson直线以与切点三角形的Euler直线平行，并且Fb关于切点三角形与中点三角形的Simson直线重合。
http://bbs.mathchina.com/cgi-bin/attachment.cgi?forum=5&topic=2068&postno=1&name=CEB4C3FCC3FB_1164420633&type=.jpg
详细讨论参考：
http://bbs.mathchina.com/cgi-bin/topic.cgi?forum=5&topic=2068 估计楼主又打算来这里“显摆”你的“机器证明”了。 定理机器证明
1、C/C++写的程序虽然速度快，但涉及到的模式太多，相对复杂
2、这里OOP思想并不占优势
3、必须用专门的语言，我觉得ML，Haskell等最合适了
Prolog主要用于知识库，lisp效率有点低。他们的特点是针对性强，程序简单 题目太复杂乐,缺乏数学美 应该属于堆砌结果的题目 晕～～～ “估计楼主又打算来这里“显摆”你的“机器证明”了。”
没有必要“显摆”，只是希望看到有志者应用论文中的新概念编写出更强大的符号计算软件，实现真正意义上的“机器证明”。复数方法更容易看出几何意义。 吴方法不可以吗
我用过两个软件,在这里显显摆了， 一个是MMP软件，
http://www.mmrc.iss.ac.cn/mmp/ ，不过几年都没更新了，
另外，Java 几何专家何专家，如果你浏览器装了jre，可以在线运行
http://www.cs.wichita.edu/~ye/gex.html
这两个都能自动推理，证明几何命题的 原帖由 无心人 于 2009-3-16 19:49 发表 http://bbs.emath.ac.cn/images/common/back.gif
应该属于堆砌结果的题目
我甚至感觉这个命题是由软件“自动发现”出来的结论 :lol
有可能
不过，数学证明涉及到理论上的难度是很大的