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

TSC999 发表于 2017-5-24 09:44:47

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

机器证明的程序如下：
Clear ;
a1 = 0 + 0I;
b1 = 1 + 0I;
c1 = a + bI;
d1 = u + vI;
e1 = s + tI;
Simplify[{0, "\!\(\*
StyleBox[\"五个圆的内侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor\
]\)", a1, b1, c1, d1, e1}]
Jd[a_, b_, c_,
d_] := ((c - d) (b Conjugate - a Conjugate) - (a -
b) (d Conjugate - c Conjugate))/((c - d) (Conjugate -
Conjugate) - (a - b) (Conjugate - Conjugate[
d])); (* 直线 AB 与 CD 的交点坐标 *)
f = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]]; (*直线 B1C1 与 D1E1 的交点坐标*)
g = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
h = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
j = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
k = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
Simplify[{1, "\!\(\*
StyleBox[\"五角星的五个顶点坐标\",\nFontSize->10,\nFontColor->RGBColor\
]\)", f, g, h, j, k}]

Wx := (
a (c - b) a\ + b (a - c) b\ +
c (b - a) c\)/((c - b) a\ + (a -
c) b\ + (b -
a) c\); (* 三角形 ABC 的外心坐标 *)
o1 = FunctionExpand,
Element[{a, b, u, v, s, t},
Reals]]; (* \A1B1J 的外心坐标 *)
o2 = FunctionExpand, Element[{a, b, u, v, s, t}, Reals]];
o3 = FunctionExpand, Element[{a, b, u, v, s, t}, Reals]];
o4 = FunctionExpand, Element[{a, b, u, v, s, t}, Reals]];
o5 = FunctionExpand, Element[{a, b, u, v, s, t}, Reals]];
Simplify[{2, "\!\(\*
StyleBox[\"五个三角形的外心坐标\",\nFontSize->10,\nFontColor->RGBColor\
]\)", o1, o2, o3, o4, o5}]

Dchd := (
b a\ - b\ a + (a - b) p\)/(
a\ - b\);(* p 点关于直线 XY 的镜像点 *)
a2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]]; (* A1点关于直线 O5O1 的镜像点 *)
b2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
c2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
d2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
e2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];
Simplify[{3, "\!\(\*
StyleBox[\"五个圆的外侧交点坐标\",\nFontSize->10,\nFontColor->RGBColor\
]\)", a2, b2, c2, d2, e2}]

Jiao :=
Simplify[((x - y) (z\ - y\))/((z -
y) (x\ - y\))];(* 定义由 x,y,z 三点构成的有向角 *)
(* 注：上面这个自定义函数，若前面不加Simplify, 运行时间极长，可能做不出来。加上后，全部运行一分钟。 *)
J1 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];(* \A2C2B2 *)
J2 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];(* \A2D2B2 *)
J3 = FunctionExpand,
Element[{a, b, u, v, s, t}, Reals]];(* \A2E2B2 *)
Simplify[{4, "\!\(\*
StyleBox[\"三个角度\",\nFontSize->10,\nFontColor->RGBColor[1, 0, \
0]]\)\!\(\*
StyleBox[\"\A2C2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"，\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"\A2D2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"，\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"\A2E2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"：\",\nFontColor->RGBColor]\)", J1, J2, J3}]

If == 0&& Simplify == 0, Print["\!\(\*
StyleBox[\"由于\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"\A2C2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"=\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"\A2D2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"=\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"\A2E2B2\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\",\",\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"故\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"A2\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"B2\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"C2\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"D2\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\",\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"E2\",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\" \",\nFontSize->10,\nFontColor->RGBColor]\)\!\(\*
StyleBox[\"五点共圆\",\nFontSize->10,\nFontColor->RGBColor]\)"]]

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

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

mathematica 发表于 2017-5-24 13:50:16

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

mathematica 发表于 2017-5-24 13:51:30

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

TSC999 发表于 2017-5-24 22:30:56

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

chyanog 发表于 2017-6-15 11:21:29

本帖最后由 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:=Circumsphere//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}]

mathematica 发表于 2021-6-18 09:30:40

chyanog 发表于 2017-6-15 11:21
做过五点共圆这个，没有用复数，Mathematica11计算耗时不到4秒

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

dlsh 发表于 2021-6-18 21:23:32

In:= 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 := Circumsphere // 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= True

Out= True
没有输出具体数值

彭翕成 发表于 2021-6-20 16:18:22

dlsh 发表于 2021-6-18 21:23
In:= Clear["`*"];

lineIntersection[{{x1_, y1_}, {x2_, y2_}, {x3_, y3_}, {x4_, y4_}}] =

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

dlsh 发表于 2021-6-20 21:45:16

本帖最后由 dlsh 于 2021-6-20 21:46 编辑

谢谢老师，看到了

页: [1]

数学研发论坛's Archiver

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