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

_only

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



机器证明的程序如下：

1. 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]]\)"]]

复制代码

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



程序代码复制以后，许多语句都改变格式了，看不懂了。有办法么？

isusesojosi

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

erileiyuqig

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

akomosuse

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

iwejinawiciru

做过五点共圆这个，没有用复数，Mathematica11计算耗时不到4秒

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}]

复制代码

uzmetub

思路在哪里？最好要有思路

euogifubize

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
没有输出具体数值

akomosuse

去掉几个分号即可。想看哪几个点，就去掉该行后面的分号

aduxoeroba

谢谢老师，看到了