免費論壇 繁體 | 簡體
Sclub交友聊天~加入聊天室當版主
分享
Board logo

标题: mathematica 机器证明平面几何定理【例 2】 [打印本页]

作者: TSC999    时间: 2017-5-29 14:46     标题: mathematica 机器证明平面几何定理【例 2】

任意画一个不等边的五角星,图中有五个三角形,它们的外接圆交于 10 个点。证明外侧的五个交点 A2, B2, C2, D2, E2 五点共圆,如图:

图一.png
2017-5-29 14:40
  1. Clear[a, b, u, v, s, t] ;      
  2. a1 = 0 + 0  I;
  3. b1 = 1 + 0  I;
  4. c1 = a + b  I;   
  5. d1 = u + v  I;
  6. e1 = s + t  I;  
  7. Simplify[{0, "\!\(\*
  8. StyleBox[\"五个圆的内侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
  9. ]\)", a1, b1, c1, d1, e1}]
  10. Jd[a_, b_, c_,
  11.   d_] := ((c - d) (b Conjugate[a] - a Conjugate[b]) - (a -
  12.      b) (d Conjugate[c] - c Conjugate[d]))/((c - d) (Conjugate[a] -
  13.      Conjugate[b]) - (a - b) (Conjugate[c] - Conjugate[
  14.      d])); (* 直线 AB 与 CD 的交点坐标 *)
  15. f = FunctionExpand[Jd[b1, c1, d1, e1],
  16.   Element[{a, b, u, v, s, t}, Reals]]; (*直线 B1C1 与 D1E1 的交点坐标*)
  17. g = FunctionExpand[Jd[c1, d1, a1, e1],
  18.   Element[{a, b, u, v, s, t}, Reals]];
  19. h = FunctionExpand[Jd[a1, b1, d1, e1],
  20.    Element[{a, b, u, v, s, t}, Reals]];
  21. j = FunctionExpand[Jd[b1, c1, a1, e1],
  22.    Element[{a, b, u, v, s, t}, Reals]];
  23. k = FunctionExpand[Jd[a1, b1, c1, d1],
  24.    Element[{a, b, u, v, s, t}, Reals]];
  25. Simplify[{1, "\!\(\*
  26. StyleBox[\"五角星的五个顶点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
  27. ]\)", f, g, h, j, k}]

  28. Wx[a_, b_, c_] := (
  29. a (c - b) a\[Conjugate] + b (a - c) b\[Conjugate] +
  30.   c (b - a) c\[Conjugate])/((c - b) a\[Conjugate] + (a -
  31.      c) b\[Conjugate] + (b -
  32.      a) c\[Conjugate]);   (* 三角形 ABC 的外心坐标 *)
  33. o1 = FunctionExpand[Wx[a1, b1, j],
  34.   Element[{a, b, u, v, s, t},
  35.    Reals]]; (* \[EmptyUpTriangle]A1B1J 的外心坐标 *)
  36. o2 = FunctionExpand[Wx[b1, c1, k], Element[{a, b, u, v, s, t}, Reals]];
  37. o3 = FunctionExpand[Wx[c1, d1, f], Element[{a, b, u, v, s, t}, Reals]];
  38. o4 = FunctionExpand[Wx[d1, e1, g], Element[{a, b, u, v, s, t}, Reals]];
  39. o5 = FunctionExpand[Wx[a1, e1, h], Element[{a, b, u, v, s, t}, Reals]];
  40. Simplify[{2, "\!\(\*
  41. StyleBox[\"五个三角形的外心坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
  42. ]\)", o1, o2, o3, o4, o5}]

  43. Dchd[p_, a_, b_] := (
  44. b a\[Conjugate] - b\[Conjugate] a + (a - b) p\[Conjugate])/(
  45. a\[Conjugate] - b\[Conjugate]);  (* p 点关于直线 XY 的镜像点 *)
  46. a2 = FunctionExpand[Dchd[a1, o5, o1],
  47.   Element[{a, b, u, v, s, t}, Reals]]; (* A1点关于直线 O5O1 的镜像点 *)
  48. b2 = FunctionExpand[Dchd[b1, o1, o2],
  49.   Element[{a, b, u, v, s, t}, Reals]];
  50. c2 = FunctionExpand[Dchd[c1, o2, o3],
  51.    Element[{a, b, u, v, s, t}, Reals]];
  52. d2 = FunctionExpand[Dchd[d1, o3, o4],
  53.    Element[{a, b, u, v, s, t}, Reals]];
  54. e2 = FunctionExpand[Dchd[e1, o4, o5],
  55.    Element[{a, b, u, v, s, t}, Reals]];
  56. Simplify[{3, "\!\(\*
  57. StyleBox[\"五个圆的外侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
  58. ]\)", a2, b2, c2, d2, e2}]

  59. Jiao[x_, y_, z_] :=
  60. Simplify[((x - y) (z\[Conjugate] - y\[Conjugate]))/((z -
  61.      y) (x\[Conjugate] - y\[Conjugate]))];  (* 定义由 x,y,z 三点构成的有向角 *)
  62. (* 注:上面这个自定义函数,若前面不加Simplify, 运行时间极长,可能做不出来。加上后,全部运行一分钟。 *)
  63. J1 = FunctionExpand[Jiao[a2, c2, b2],
  64.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2C2B2 *)
  65. J2 = FunctionExpand[Jiao[a2, d2, b2],
  66.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2D2B2 *)
  67. J3 = FunctionExpand[Jiao[a2, e2, b2],
  68.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2E2B2 *)
  69. Simplify[{4, "\!\(\*
  70. StyleBox[\"三个角度\",\nFontSize->10,\nFontColor->RGBColor[1, 0, \
  71. 0]]\)\!\(\*
  72. StyleBox[\"\[Angle]A2C2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  73. StyleBox[\",\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  74. StyleBox[\"\[Angle]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  75. StyleBox[\",\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  76. StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  77. StyleBox[\":\",\nFontColor->RGBColor[0, 0, 1]]\)", J1, J2, J3}]

  78. If[Simplify[J1 - J2] == 0  && Simplify[J1 - J3] == 0, Print["\!\(\*
  79. StyleBox[\"由于\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  80. StyleBox[\"\[Angle]A2C2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  81. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  82. StyleBox[\"=\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  83. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  84. StyleBox[\"\[Angle]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  85. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  86. StyleBox[\"=\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  87. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  88. StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
  89. StyleBox[\",\",\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  90. StyleBox[\"故\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  91. StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  92. StyleBox[\"A2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  93. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  94. StyleBox[\"B2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  95. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  96. StyleBox[\"C2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  97. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  98. StyleBox[\"D2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  99. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  100. StyleBox[\"E2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  101. StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
  102. StyleBox[\"五点共圆\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)"]]
复制代码
程序运行近一分钟,给出如下证明:
图二.png
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