账号 自动登录 找回密码 密码 欢迎注册
 搜索

# [分享] mathematica 机器证明平面几何定理【例 2】

### 马上注册，结交更多好友，享用更多功能，让你轻松玩转社区。

×

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]]$$"]]

 可以给程序多加点注释,容易看明白,我觉得五点共圆很有意思

 机器证明很有价值,能节省脑力,几何问题代数化,有意思

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

 本帖最后由 chyanog 于 2017-6-15 11:37 编辑 做过五点共圆这个，没有用复数，Mathematica11计算耗时不到4秒 Clear["*"]; lineIntersection[{{x1_,y1_},{x2_,y2_},{x3_,y3_},{x4_,y4_}}]=   Solve[{Det[{{x,y,1},{x1,y1,1},{x2,y2,1}}],Det[{{x,y,1},{x3,y3,1},{x4,y4,1}}]}==0,{x,y}]//First//Values; reflect[{{x0_,y0_},{x1_,y1_},{x2_,y2_}}]=   Solve[{Det[{{x1,y1,1},{x2,y2,1},{(x0+x)/2,(y0+y)/2,1}}],({x,y}-{x0,y0}).({x1,y1}-{x2,y2})}==0,{x,y}]//First//Values; threePointCircle[p_]:=Circumsphere[p]//First; fourPointOnCircle[{{x1_, y1_}, {x2_, y2_}, {x3_, y3_}, {x4_, y4_}}] :=   Det[{{x1^2+y1^2,x1,y1,1},{x2^2+y2^2,x2,y2,1},{x3^2+y3^2,x3,y3,1},{x4^2+y4^2,x4,y4,1}}]==0//Simplify; {B1,B2,B3,B4,B5}={{0,0},{x1,y1},{x2,y2},{x3,y3},{1,0}}; {A1,A2,A3,A4,A5}=lineIntersection/@{{B1,B2,B4,B5},{B1,B5,B2,B3},{B1,B2,B3,B4},{B2,B3,B4,B5},{B1,B5,B3,B4}}; {O1,O2,O3,O4,O5}=threePointCircle/@{{A1,B1,B5},{A2,B1,B2},{A3,B2,B3},{A4,B3,B4},{A5,B4,B5}}; (*五三角形的外心坐标*) {C1,C2,C3,C4,C5}=reflect/@{{B1,O1,O2},{B2,O2,O3},{B3,O3,O4},{B4,O4,O5},{B5,O5,O1}}//Simplify; (*五圆外侧交点坐标*) fourPointOnCircle[{C1,C2,C3,C4}] fourPointOnCircle[{C2,C3,C4,C5}]复制代码

 chyanog 发表于 2017-6-15 11:21 做过五点共圆这个，没有用复数，Mathematica11计算耗时不到4秒 思路在哪里？最好要有思路

 In[1]:= Clear["*"]; lineIntersection[{{x1_, y1_}, {x2_, y2_}, {x3_, y3_}, {x4_, y4_}}] =   Solve[{Det[{{x, y, 1}, {x1, y1, 1}, {x2, y2, 1}}],        Det[{{x, y, 1}, {x3, y3, 1}, {x4, y4, 1}}]} == 0, {x, y}] //     First // Values; reflect[{{x0_, y0_}, {x1_, y1_}, {x2_, y2_}}] =   Solve[{Det[{{x1, y1, 1}, {x2, y2, 1}, {(x0 + x)/2, (y0 + y)/2,           1}}], ({x, y} - {x0, y0}).({x1, y1} - {x2, y2})} == 0, {x,       y}] // First // Values; threePointCircle[p_] := Circumsphere[p] // First; fourPointOnCircle[{{x1_, y1_}, {x2_, y2_}, {x3_, y3_}, {x4_, y4_}}] :=    Det[{{x1^2 + y1^2, x1, y1, 1}, {x2^2 + y2^2, x2, y2,        1}, {x3^2 + y3^2, x3, y3, 1}, {x4^2 + y4^2, x4, y4, 1}}] == 0 //     Simplify; {B1, B2, B3, B4, B5} = {{0, 0}, {x1, y1}, {x2, y2}, {x3, y3}, {1, 0}}; {A1, A2, A3, A4, A5} =   lineIntersection /@ {{B1, B2, B4, B5}, {B1, B5, B2, B3}, {B1, B2,      B3, B4}, {B2, B3, B4, B5}, {B1, B5, B3, B4}}; {O1, O2, O3, O4, O5} = threePointCircle /@ {{A1, B1, B5}, {A2, B1, B2}, {A3, B2, B3}, {A4,     B3, B4}, {A5, B4, B5}};(*五三角形的外心坐标*){C1, C2, C3, C4, C5} = reflect /@ {{B1, O1, O2}, {B2, O2, O3}, {B3, O3, O4}, {B4, O4,      O5}, {B5, O5, O1}} // Simplify;(*五圆外侧交点坐标*)fourPointOnCircle[{C1,    C2, C3, C4}] fourPointOnCircle[{C2, C3, C4, C5}] Out[8]= True Out[9]= True 没有输出具体数值

 dlsh 发表于 2021-6-18 21:23 In[1]:= Clear["`*"]; lineIntersection[{{x1_, y1_}, {x2_, y2_}, {x3_, y3_}, {x4_, y4_}}] = 去掉几个分号即可。想看哪几个点，就去掉该行后面的分号

 本帖最后由 dlsh 于 2021-6-20 21:46 编辑 谢谢老师，看到了

 您需要登录后才可以回帖 登录 | 欢迎注册 本版积分规则 回帖并转播 回帖后跳转到最后一页

GMT+8, 2024-2-26 09:10 , Processed in 0.061668 second(s), 19 queries .

Powered by Discuz! X3.5

© 2001-2024 Discuz! Team.