mathematica 机器证明平面几何定理【例 4】
本帖最后由 TSC999 于 2017-5-25 07:37 编辑下图摘自：宁波东方热线教育论坛（网址 http://bbs.cnool.net/cforum-494.html），一个神秘奇人史勇的作品。
上面这个构图方法很是奇特，据说有一套理论。
可供复制的程序代码如下：
D1 = (e + f - d)/(e f); E1 = (f + d - e)/(f d); F1 = (d + e - f)/(
d e);(* 镜像点 D1,E1,F1 的复坐标。此公式成立的条件是 D1,E1,F1 全在单位圆周上 *)
O1 = (2 (d^2 + e^2 + f^2))/(
d^2 (e + f) + e f (e + f) +
d (e^2 - e f + f^2));(* \D1E1F1 的外心坐标。 *)
G1 = (2 d e + 2 e f + 2 d f - d^2 - e^2 - f^2)/(
3 d e f);(* \D1E1F1 的重心坐标。 *)
H1 = (-d^4 (e + f) - e^4 (f + d) - f^4 (d + e) +
d^3 (e^2 + f^2 + e f) + e^3 (f^2 + d^2 + f d) +
f^3 (d^2 + e^2 + d e ))/(
d e f (d^2 (e + f) + e^2 (f + d) + f^2 (d + e) -
d e f));(* \D1E1F1 的垂心坐标。 *)
N0 =((d + e +
f)^2)/((d + e) (d + f) (e +
f)); (* \A0B0C0 的九点圆圆心坐标。 *)
\!\(\*OverscriptBox[\(e\), \(_\)]\) = 1/e;
\!\(\*OverscriptBox[\(f\), \(_\)]\) = 1/f;
\!\(\*OverscriptBox[\(d\), \(_\)]\) =
1/d; (* 上面有横线的字母表示共轭复数。此句若去掉，结果中会出现许多上面带横线的字母。 *)
\!\(\*OverscriptBox[\(O1\), \(_\)]\) = Simplify[O1 /. {d ->
\!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
\!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
\!\(\*OverscriptBox[\(f\), \(_\)]\)}];
\!\(\*OverscriptBox[\(G1\), \(_\)]\) = Simplify[G1 /. {d ->
\!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
\!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
\!\(\*OverscriptBox[\(f\), \(_\)]\)}];
\!\(\*OverscriptBox[\(H1\), \(_\)]\) = Simplify[H1 /. {d ->
\!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
\!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
\!\(\*OverscriptBox[\(f\), \(_\)]\)}];
\!\(\*OverscriptBox[\(N0\), \(_\)]\) = Simplify[N0 /. {d ->
\!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
\!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
\!\(\*OverscriptBox[\(f\), \(_\)]\)}];
Simplify[{
\!\(\*OverscriptBox[\(O1\), \(_\)]\),
\!\(\*OverscriptBox[\(G1\), \(_\)]\),
\!\(\*OverscriptBox[\(H1\), \(_\)]\),
\!\(\*OverscriptBox[\(N0\), \(_\)]\)}]
Simplify[{1, (O1 - G1)/(
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\)), (H1 - N0)/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\)) - (H1 - N0)/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\))}]
Factor[{2, (O1 - G1)/(
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\)), (H1 - N0)/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\)) - (H1 - N0)/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\))}]
Simplify[{3, (O1 - G1)/(H1 - N0), (
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(H1 - N0) - (
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\))}]\
(*如果(O1-G1)/(H1-N0)-(Overscript-Overscript[G1, \
_])/(Overscript-Overscript)=0,四点共线*)
IF[(O1 - G1)/(H1 - N0) - (
\!\(\*OverscriptBox[\(O1\), \(_\)]\) -
\!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
\!\(\*OverscriptBox[\(H1\), \(_\)]\) -
\!\(\*OverscriptBox[\(N0\), \(_\)]\)) == 0,
Print["由于 \!\(\*FractionBox[\(O1 - G1\), \(H1 - \
N0\)]\)-\!\(\*FractionBox[\(\*OverscriptBox[\(O1\), \(_\)] - \
\*OverscriptBox[\(G1\), \(_\)]\), \(\*OverscriptBox[\(H1\), \(_\)] - \
\*OverscriptBox[\(N0\), \(_\)]\)]\) =0，所以 O1,G1,H1,N0 四点共线。"]];
程序运行结果如下：
这只能说是计算机辅助计算，不能算机器证明 这个史勇早年在百度几何吧一直很活跃，他自创的理论有时候可以很简单地证明某些复杂的问题，下面帖子中的内容他在很多地方都宣传过，只是他的理论感觉总有点别扭，细节论述地不够踏实，让人不放心。他自己说是用到了射影几何的一些东西，@hujunhua 能否看看里面的理论基础是否牢固，或是其本质等价的东西是什么？
http://bbs.cnool.net/cthread-105628438.html 比如其图一中数偶坐标的定义。
我们总可以做射影变换将图中二次曲线$Omega$变换为抛物线$x^2=2y$而且将视点S变换为y轴无穷远点。
而图一中x轴我们可以看成变换后直角坐标系的x轴。
于是我们容易计算得出上面抛物线上横坐标为$x_1,x_2$的两个点处切线的交点坐标为$({x_1+x_2}/2,{x_1x_2}/2)$,这就是其数偶的来源。
页:
[1]