数学研发网设为首页收藏本站
切换到窄版

 找回密码
 欢迎注册
数学研发论坛»论坛 › 【数学研究】 › 数学软件 › mathematica 机器证明平面几何定理【例 4】 ...
返回列表 发新帖
查看: 9375|回复: 10

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

[复制链接]
TSC999
发表于 2017-5-25 06:51:21 | 显示全部楼层 |阅读模式

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

您需要 登录 才可以下载或查看，没有账号？欢迎注册

×
本帖最后由 TSC999 于 2017-5-25 07:37 编辑

下图摘自：宁波东方热线教育论坛（网址 http://bbs.cnool.net/cforum-494.html），一个神秘奇人史勇的作品。
N 点在欧拉上.png

上面这个构图方法很是奇特，据说有一套理论。
毋因群疑而阻独见　　毋任己意而废人言
毋私小惠而伤大体　　毋借公论以快私情
回复

使用道具 举报

TSC999
 楼主| 发表于 2017-5-25 07:14:10 | 显示全部楼层
N 点在欧拉上程序图片.png

可供复制的程序代码如下：

  1. D1 = (e + f - d)/(e f); E1 = (f + d - e)/(f d); F1 = (d + e - f)/(
  2. d e);  (* 镜像点 D1,E1,F1 的复坐标。此公式成立的条件是 D1,E1,F1 全在单位圆周上 *)
  3. O1 = (2 (d^2 + e^2 + f^2))/(
  4.   d^2 (e + f) + e f (e + f) +
  5.    d (e^2 - e f + f^2));  (* \[EmptyUpTriangle]D1E1F1 的外心坐标。 *)
  6. G1 = (2 d e + 2 e f + 2 d f - d^2 - e^2 - f^2)/(
  7.   3 d e f);  (* \[EmptyUpTriangle]D1E1F1 的重心坐标。 *)
  8. H1 = (-d^4 (e + f) - e^4 (f + d) - f^4 (d + e) +
  9.    d^3 (e^2 + f^2 + e f) + e^3 (f^2 + d^2 + f d) +
  10.    f^3 (d^2 + e^2 + d e ))/(
  11.   d e f (d^2 (e + f) + e^2 (f + d) + f^2 (d + e) -
  12.      d e f));  (* \[EmptyUpTriangle]D1E1F1 的垂心坐标。 *)
  13. N0 =  ((d + e +
  14.     f)^2)/((d + e) (d + f) (e +
  15.      f));     (* \[EmptyUpTriangle]A0B0C0 的九点圆圆心坐标。 *)


  18. \!\(\*OverscriptBox[\(e\), \(_\)]\) = 1/e;
  19. \!\(\*OverscriptBox[\(f\), \(_\)]\) = 1/f;
  20. \!\(\*OverscriptBox[\(d\), \(_\)]\) =
  21. 1/d;    (* 上面有横线的字母表示共轭复数。此句若去掉，结果中会出现许多上面带横线的字母。 *)


  24. \!\(\*OverscriptBox[\(O1\), \(_\)]\) = Simplify[O1 /. {d ->
  25. \!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
  26. \!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
  27. \!\(\*OverscriptBox[\(f\), \(_\)]\)}];

  29. \!\(\*OverscriptBox[\(G1\), \(_\)]\) = Simplify[G1 /. {d ->
  30. \!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
  31. \!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
  32. \!\(\*OverscriptBox[\(f\), \(_\)]\)}];

  34. \!\(\*OverscriptBox[\(H1\), \(_\)]\) = Simplify[H1 /. {d ->
  35. \!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
  36. \!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
  37. \!\(\*OverscriptBox[\(f\), \(_\)]\)}];

  39. \!\(\*OverscriptBox[\(N0\), \(_\)]\) = Simplify[N0 /. {d ->
  40. \!\(\*OverscriptBox[\(d\), \(_\)]\), e ->
  41. \!\(\*OverscriptBox[\(e\), \(_\)]\), f ->
  42. \!\(\*OverscriptBox[\(f\), \(_\)]\)}];

  44. Simplify[{
  45. \!\(\*OverscriptBox[\(O1\), \(_\)]\),
  46. \!\(\*OverscriptBox[\(G1\), \(_\)]\),
  47. \!\(\*OverscriptBox[\(H1\), \(_\)]\),
  48. \!\(\*OverscriptBox[\(N0\), \(_\)]\)}]
  49. Simplify[{1, (O1 - G1)/(
  50. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  51. \!\(\*OverscriptBox[\(G1\), \(_\)]\)), (H1 - N0)/(
  52. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  53. \!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(
  54. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  55. \!\(\*OverscriptBox[\(G1\), \(_\)]\)) - (H1 - N0)/(
  56. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  57. \!\(\*OverscriptBox[\(N0\), \(_\)]\))}]
  58. Factor[{2, (O1 - G1)/(
  59. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  60. \!\(\*OverscriptBox[\(G1\), \(_\)]\)), (H1 - N0)/(
  61. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  62. \!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(
  63. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  64. \!\(\*OverscriptBox[\(G1\), \(_\)]\)) - (H1 - N0)/(
  65. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  66. \!\(\*OverscriptBox[\(N0\), \(_\)]\))}]
  67. Simplify[{3, (O1 - G1)/(H1 - N0), (
  68. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  69. \!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
  70. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  71. \!\(\*OverscriptBox[\(N0\), \(_\)]\)), (O1 - G1)/(H1 - N0) - (
  72. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  73. \!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
  74. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  75. \!\(\*OverscriptBox[\(N0\), \(_\)]\))}]  \
  76. (*如果(O1-G1)/(H1-N0)-(Overscript[O1, _]-Overscript[G1, \
  77. _])/(Overscript[H1, _]-Overscript[N0, _])=0,四点共线*)
  78. IF[(O1 - G1)/(H1 - N0) - (
  79. \!\(\*OverscriptBox[\(O1\), \(_\)]\) -
  80. \!\(\*OverscriptBox[\(G1\), \(_\)]\))/(
  81. \!\(\*OverscriptBox[\(H1\), \(_\)]\) -
  82. \!\(\*OverscriptBox[\(N0\), \(_\)]\)) == 0,
  83.   Print["由于 \!\(\*FractionBox[\(O1 - G1\), \(H1 - \
  84. N0\)]\)-\!\(\*FractionBox[\(\*OverscriptBox[\(O1\), \(_\)] - \
  85. \*OverscriptBox[\(G1\), \(_\)]\), \(\*OverscriptBox[\(H1\), \(_\)] - \
  86. \*OverscriptBox[\(N0\), \(_\)]\)]\) =0，所以 O1,G1,H1,N0 四点共线。"]];
  87.   
复制代码


程序运行结果如下：

程序运行结果：.png

点评

chyanog
楼主可以试试这个问题，https://www.research.ibm.com/haifa/ponderthis/challenges/August1998.html  发表于 2017-5-31 15:22
mathematica
少发图片,要不然有人会不高兴的  发表于 2017-5-25 09:36
TSC999
程序运行时间很短，约 2 秒钟。  发表于 2017-5-25 07:16
毋因群疑而阻独见　　毋任己意而废人言
毋私小惠而伤大体　　毋借公论以快私情
回复 支持 反对

使用道具 举报

mathe
发表于 2017-5-25 08:40:23 | 显示全部楼层
这只能说是计算机辅助计算，不能算机器证明
毋因群疑而阻独见　　毋任己意而废人言
毋私小惠而伤大体　　毋借公论以快私情
回复 支持 反对

使用道具 举报

kastin
发表于 2017-6-5 10:38:35 | 显示全部楼层
这个史勇早年在百度几何吧一直很活跃，他自创的理论有时候可以很简单地证明某些复杂的问题，下面帖子中的内容他在很多地方都宣传过，只是他的理论感觉总有点别扭，细节论述地不够踏实，让人不放心。他自己说是用到了射影几何的一些东西，@hujunhua 能否看看里面的理论基础是否牢固，或是其本质等价的东西是什么？
http://bbs.cnool.net/cthread-105628438.html

点评

mathe
我看不出有任何理由要抛弃传统的大家熟悉的直角坐标系的表示方法，而采用他的非线性的方案，毕竟他是通过大量的计算来达到他的目的的，我不觉得他的方案的计算量会比用直角坐标系小  发表于 2017-6-5 11:52
mathe
其实就是射影几何的简单坐标变换。只要将平面上任意一条基本圆锥曲线通过射影变换转为为曲线x^2=2y. 然后在变换后的平面上，做坐标变换x=uv, y=u+v,也就得出了他的坐标u X v  发表于 2017-6-5 11:49
毋因群疑而阻独见　　毋任己意而废人言
毋私小惠而伤大体　　毋借公论以快私情
回复 支持 反对

使用道具 举报

mathe
发表于 2017-6-5 14:29:13 | 显示全部楼层
比如其图一中数偶坐标的定义。
我们总可以做射影变换将图中二次曲线$Omega$变换为抛物线$x^2=2y$而且将视点S变换为y轴无穷远点。
而图一中x轴我们可以看成变换后直角坐标系的x轴。
于是我们容易计算得出上面抛物线上横坐标为$x_1,x_2$的两个点处切线的交点坐标为$({x_1+x_2}/2,{x_1x_2}/2)$,这就是其数偶的来源。

点评

kastin
我觉得他是为了类似用复数来表示空间点的那种方式来研究二次曲线几何问题，然后通过这种特殊的记号方式，计算后得到一种有规律的代数表达。或者说是一种代数运算的“翻译”。  发表于 2017-6-5 16:04
毋因群疑而阻独见　　毋任己意而废人言
毋私小惠而伤大体　　毋借公论以快私情
回复 支持 反对

使用道具 举报

返回列表 发新帖
高级模式
B Color Image Link Quote Code Smilies
您需要登录后才可以回帖 登录 | 欢迎注册

本版积分规则

小黑屋|手机版|数学研发网 ( 苏ICP备07505100号 )

GMT+8, 2024-4-19 12:58 , Processed in 0.056331 second(s), 20 queries .

Powered by Discuz! X3.5

© 2001-2024 Discuz! Team.

快速回复 返回顶部 返回列表