mathematica 机器证明平面几何定理【例 2】

TSC999

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

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}]
29. Wx[a_, b_, c_] := (
30. a (c - b) a\[Conjugate] + b (a - c) b\[Conjugate] +
31.   c (b - a) c\[Conjugate])/((c - b) a\[Conjugate] + (a -
32.      c) b\[Conjugate] + (b -
33.      a) c\[Conjugate]);   (* 三角形 ABC 的外心坐标 *)
34. o1 = FunctionExpand[Wx[a1, b1, j],
35.   Element[{a, b, u, v, s, t},
36.    Reals]]; (* \[EmptyUpTriangle]A1B1J 的外心坐标 *)
37. o2 = FunctionExpand[Wx[b1, c1, k], Element[{a, b, u, v, s, t}, Reals]];
38. o3 = FunctionExpand[Wx[c1, d1, f], Element[{a, b, u, v, s, t}, Reals]];
39. o4 = FunctionExpand[Wx[d1, e1, g], Element[{a, b, u, v, s, t}, Reals]];
40. o5 = FunctionExpand[Wx[a1, e1, h], Element[{a, b, u, v, s, t}, Reals]];
41. Simplify[{2, "\!\(\*
42. StyleBox[\"五个三角形的外心坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
43. ]\)", o1, o2, o3, o4, o5}]
45. Dchd[p_, a_, b_] := (
46. b a\[Conjugate] - b\[Conjugate] a + (a - b) p\[Conjugate])/(
47. a\[Conjugate] - b\[Conjugate]);  (* p 点关于直线 XY 的镜像点 *)
48. a2 = FunctionExpand[Dchd[a1, o5, o1],
49.   Element[{a, b, u, v, s, t}, Reals]]; (* A1点关于直线 O5O1 的镜像点 *)
50. b2 = FunctionExpand[Dchd[b1, o1, o2],
51.   Element[{a, b, u, v, s, t}, Reals]];
52. c2 = FunctionExpand[Dchd[c1, o2, o3],
53.    Element[{a, b, u, v, s, t}, Reals]];
54. d2 = FunctionExpand[Dchd[d1, o3, o4],
55.    Element[{a, b, u, v, s, t}, Reals]];
56. e2 = FunctionExpand[Dchd[e1, o4, o5],
57.    Element[{a, b, u, v, s, t}, Reals]];
58. Simplify[{3, "\!\(\*
59. StyleBox[\"五个圆的外侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]\
60. ]\)", a2, b2, c2, d2, e2}]
62. Jiao[x_, y_, z_] :=
63. Simplify[((x - y) (z\[Conjugate] - y\[Conjugate]))/((z -
64.      y) (x\[Conjugate] - y\[Conjugate]))];  (* 定义由 x,y,z 三点构成的有向角 *)
65. (* 注：上面这个自定义函数，若前面不加Simplify, 运行时间极长，可能做不出来。加上后，全部运行一分钟。 *)
66. J1 = FunctionExpand[Jiao[a2, c2, b2],
67.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2C2B2 *)
68. J2 = FunctionExpand[Jiao[a2, d2, b2],
69.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2D2B2 *)
70. J3 = FunctionExpand[Jiao[a2, e2, b2],
71.   Element[{a, b, u, v, s, t}, Reals]];  (* \[Angle]A2E2B2 *)
72. Simplify[{4, "\!\(\*
73. StyleBox[\"三个角度\",\nFontSize->10,\nFontColor->RGBColor[1, 0, \
74. 0]]\)\!\(\*
75. StyleBox[\"\[Angle]A2C2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
76. StyleBox[\"，\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
77. StyleBox[\"\[Angle]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
78. StyleBox[\"，\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
79. StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
80. StyleBox[\"：\",\nFontColor->RGBColor[0, 0, 1]]\)", J1, J2, J3}]
82. If[Simplify[J1 - J2] == 0  && Simplify[J1 - J3] == 0, Print["\!\(\*
83. StyleBox[\"由于\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
84. StyleBox[\"\[Angle]A2C2B2\",\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]A2D2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
89. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
90. StyleBox[\"=\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
91. StyleBox[\" \",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
92. StyleBox[\"\[Angle]A2E2B2\",\nFontColor->RGBColor[0, 0, 1]]\)\!\(\*
93. StyleBox[\",\",\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
94. StyleBox[\"故\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
95. StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
96. StyleBox[\"A2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
97. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
98. StyleBox[\"B2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
99. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
100. StyleBox[\"C2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
101. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
102. StyleBox[\"D2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
103. StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
104. StyleBox[\"E2\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
105. StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)\!\(\*
106. StyleBox[\"五点共圆\",\nFontSize->10,\nFontColor->RGBColor[1, 0, 0]]\)"]]

Copy the Code

程序运行近一分钟，给出如下证明：

TSC999

这个机器证明的思路是向李涛学来的。李涛的导师是张景中。李涛作了一套机器证明的软件，这软件我是不知道的，但是软件的原理就体现在上面这个程序设计。
机器证明的难点，一是如何构图，构图要使得各关键点的坐标容易算出。第二，要积累一些平面几何的公式。第三，软件平台是 mathematica，软件的计算能力应该足够强大。

有网友认为，这个还不能算是真正的机器证明，只能算是计算机辅助计算。这样说也可以，再等一些年，人工智能发展了，只须让机器瞄一眼题目，它就能够一瞬间给出纯几何证明和代数计算证明。

isee

kuing.cjhb.site/forum.php?mod=viewthread&tid=274

继续“科谱”，嘿嘿