繁體
|
簡體
Sclub交友聊天~加入聊天室當版主
(檢舉)
分享
新浪微博
QQ空间
人人网
腾讯微博
Facebook
Google+
Plurk
Twitter
Line
标题:
mathematica 机器证明平面几何定理【例 2】
[打印本页]
作者:
TSC999
时间:
2017-5-29 14:46
标题:
mathematica 机器证明平面几何定理【例 2】
任意画一个不等边的五角星,图中有五个三角形,它们的外接圆交于 10 个点。证明外侧的五个交点 A2, B2, C2, D2, E2 五点共圆,如图:
2017-5-29 14:40
Clear[a, b, u, v, s, t] ;
a1 = 0 + 0 I;
b1 = 1 + 0 I;
c1 = a + b I;
d1 = u + v I;
e1 = s + t I;
Simplify[{0, "\!\(\*
StyleBox[\"五个圆的内侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
]\)", a1, b1, c1, d1, e1}]
Jd[a_, b_, c_,
d_] := ((c - d) (b Conjugate[a] - a Conjugate[b]) - (a -
b) (d Conjugate[c] - c Conjugate[d]))/((c - d) (Conjugate[a] -
Conjugate[b]) - (a - b) (Conjugate[c] - Conjugate[
d])); (* 直线 AB 与 CD 的交点坐标 *)
f = FunctionExpand[Jd[b1, c1, d1, e1],
Element[{a, b, u, v, s, t}, Reals]]; (*直线 B1C1 与 D1E1 的交点坐标*)
g = FunctionExpand[Jd[c1, d1, a1, e1],
Element[{a, b, u, v, s, t}, Reals]];
h = FunctionExpand[Jd[a1, b1, d1, e1],
Element[{a, b, u, v, s, t}, Reals]];
j = FunctionExpand[Jd[b1, c1, a1, e1],
Element[{a, b, u, v, s, t}, Reals]];
k = FunctionExpand[Jd[a1, b1, c1, d1],
Element[{a, b, u, v, s, t}, Reals]];
Simplify[{1, "\!\(\*
StyleBox[\"五角星的五个顶点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
]\)", f, g, h, j, k}]
Wx[a_, b_, c_] := (
a (c - b) a\[Conjugate] + b (a - c) b\[Conjugate] +
c (b - a) c\[Conjugate])/((c - b) a\[Conjugate] + (a -
c) b\[Conjugate] + (b -
a) c\[Conjugate]); (* 三角形 ABC 的外心坐标 *)
o1 = FunctionExpand[Wx[a1, b1, j],
Element[{a, b, u, v, s, t},
Reals]]; (* \[EmptyUpTriangle]A1B1J 的外心坐标 *)
o2 = FunctionExpand[Wx[b1, c1, k], Element[{a, b, u, v, s, t}, Reals]];
o3 = FunctionExpand[Wx[c1, d1, f], Element[{a, b, u, v, s, t}, Reals]];
o4 = FunctionExpand[Wx[d1, e1, g], Element[{a, b, u, v, s, t}, Reals]];
o5 = FunctionExpand[Wx[a1, e1, h], Element[{a, b, u, v, s, t}, Reals]];
Simplify[{2, "\!\(\*
StyleBox[\"五个三角形的外心坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
]\)", o1, o2, o3, o4, o5}]
Dchd[p_, a_, b_] := (
b a\[Conjugate] - b\[Conjugate] a + (a - b) p\[Conjugate])/(
a\[Conjugate] - b\[Conjugate]); (* p 点关于直线 XY 的镜像点 *)
a2 = FunctionExpand[Dchd[a1, o5, o1],
Element[{a, b, u, v, s, t}, Reals]]; (* A1点关于直线 O5O1 的镜像点 *)
b2 = FunctionExpand[Dchd[b1, o1, o2],
Element[{a, b, u, v, s, t}, Reals]];
c2 = FunctionExpand[Dchd[c1, o2, o3],
Element[{a, b, u, v, s, t}, Reals]];
d2 = FunctionExpand[Dchd[d1, o3, o4],
Element[{a, b, u, v, s, t}, Reals]];
e2 = FunctionExpand[Dchd[e1, o4, o5],
Element[{a, b, u, v, s, t}, Reals]];
Simplify[{3, "\!\(\*
StyleBox[\"五个圆的外侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
]\)", a2, b2, c2, d2, e2}]
Jiao[x_, y_, z_] :=
Simplify[((x - y) (z\[Conjugate] - y\[Conjugate]))/((z -
y) (x\[Conjugate] - y\[Conjugate]))]; (* 定义由 x,y,z 三点构成的有向角 *)
(* 注:上面这个自定义函数,若前面不加Simplify, 运行时间极长,可能做不出来。加上后,全部运行一分钟。 *)
J1 = FunctionExpand[Jiao[a2, c2, b2],
Element[{a, b, u, v, s, t}, Reals]]; (* \[Angle]A2C2B2 *)
J2 = FunctionExpand[Jiao[a2, d2, b2],
Element[{a, b, u, v, s, t}, Reals]]; (* \[Angle]A2D2B2 *)
J3 = FunctionExpand[Jiao[a2, e2, b2],
Element[{a, b, u, v, s, t}, Reals]]; (* \[Angle]A2E2B2 *)
Simplify[{4, "\!\(\*
StyleBox[\"三个角度\",\nFontSize->10,\nFontColor->RGBColor[1, 0, \
0]]\)\!\(\*
StyleBox[\"\[Angle]A2C2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\",\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"\[Angle]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\",\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\":\",\nFontColor->RGBColor[0, 0, 1]]\)", J1, J2, J3}]
If[Simplify[J1 - J2] == 0 && Simplify[J1 - J3] == 0, Print["\!\(\*
StyleBox[\"由于\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"\[Angle]A2C2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"=\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"\[Angle]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"=\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
StyleBox[\",\",\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"故\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"A2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"B2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"C2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"D2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"E2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
StyleBox[\"五点共圆\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)"]]
复制代码
程序运行近一分钟,给出如下证明:
2017-5-29 14:46
图片附件:
图一.png
(2017-5-29 14:40, 52.64 KB) / 下载次数 323
http://kuing.orzweb.net/attachment.php?aid=5008&k=5c89ca06e6ca1a715ac75899835e95b0&t=1711700736&sid=DlAdtt
图片附件:
图二.png
(2017-5-29 14:46, 318.49 KB) / 下载次数 353
http://kuing.orzweb.net/attachment.php?aid=5009&k=9284c1358418a4d9e1ada5594338d723&t=1711700736&sid=DlAdtt
作者:
TSC999
时间:
2017-5-29 14:48
本帖最后由 TSC999 于 2017-5-29 14:52 编辑
这个机器证明的思路是向李涛学来的。李涛的导师是张景中。李涛作了一套机器证明的软件,这软件我是不知道的,但是软件的原理就体现在上面这个程序设计。
机器证明的难点,一是如何构图,构图要使得各关键点的坐标容易算出。第二,要积累一些平面几何的公式。第三,软件平台是 mathematica,软件的计算能力应该足够强大。
有网友认为,这个还不能算是真正的机器证明,只能算是计算机辅助计算。这样说也可以,再等一些年,人工智能发展了,只须让机器瞄一眼题目,它就能够一瞬间给出纯几何证明和代数计算证明。
作者:
isee
时间:
2017-6-3 17:02
本帖最后由 isee 于 2017-6-3 17:03 编辑
http://kuing.orzweb.net/viewthread.php?tid=274
继续“科谱”,嘿嘿
欢迎光临 悠闲数学娱乐论坛(第2版) (http://kuing.orzweb.net/)
Powered by Discuz! 7.2