【分享】交流一下 Mathematica 编程方法，期望学习该软件的网友积极参与

天山草

[这个贴子最后由天山草在 2013/11/22 00:43pm 第 3 次编辑]

下面引用由denglongshan在 2013/11/21 09:44pm 发表的内容：
张景中利用它已经证明了，说明我们的方法还有问题，也就是说算法不好。

是的，是的，我的方法不能算是证明，只能算是验证。不知道张景中是如何用复数法证明的？
我的方法的问题在于：【1】两个相切圆的圆心坐标要用 mathematica 解方程求出，降低了程序的可读性。程序的“可读性”不知是如何评定的？要求读者既要看懂程序的运行结果，也要看懂程序本身吗？【2】用两段折线的斜率是否相等来判定三个点是否在一条直线上，方法可以，但是斜率的表达式太复杂，mathematica 吃不消，它不敢判定那两个表达式是不是恒等的。这时只能代入具体数字进行验算，结果可以准确到任意多位（此时输入的数字必须是分数，不能是小数，否则算出的结果有效数字位数很少。）但是代入具体数字计算，就差不多成了“验证”，至少是证明不算优美。如何解决这问题呢？出路一：改进构图方法，使表达式变得简单。出路二：软件平台 mathematica 增强功能，对于复杂的表达式也能处理。

denglongshan

   我也想知道张院士如何证明的，他的论文中泰博定理证明还不到5秒，而五圆定理用了20多秒。这是否说明泰博定理更简单？
   可读性指读者对证明过程更容易读懂，按照李洪波教授的观点，就是证明过程象书本上那样写出来。我的理解不必懂程序，但是程序应该输出证明定理的证据，也就是相关的数据，例如对五圆定理来说，那些点和角的有关结果，张院士的论文没有说明角相等的数据，这一点我认为可读性差，我怀疑是这个结果比较复杂，或者是忘记写出来。

下面引用由天山草在 2013/11/22 10:31am 发表的内容：
内心公式容易推出来。当然也是借助于 mathematica 这个拐棍弄出来的。
XO2 和 XO3 的公式也是借助于 mathematica 解方程求出的。各有两个解，一个解对应于相切圆较小，位于三角形外接圆的里面，这个解符合要求； ...

  不明白如何判断XO2 和 XO3 的哪两个解在圆内，从几何构图看两个解都可以在外接圆内，为什么按照你的方程，我用Mathematica求解，比你的结果复杂得多?
  求解内心时如何判断你的解不是旁心？吴文俊在《初等几何的机器证明原理》，已经指出内心求解比较困难。
   我们的证明有时计算不下去，是因为表达式中带根号。吴文俊在证明费尔巴哈定理时，为证明内切圆和外接圆的差等于两圆心的距离，采用等式两边平方的办法去根号。是否可以借鉴？[br][br]-=-=-=-=- 以下内容由 denglongshan 在 时添加 -=-=-=-=-
如果有时间可以试试论文中的其它几条定理[br][br]-=-=-=-=- 以下内容由 denglongshan 在 时添加 -=-=-=-=-
按照你的作法，认真作图，的确xO2有一个圆心在圆外。问题是如何排除？

天山草

下面引用由denglongshan在 2013/11/22 10:39pm 发表的内容：
不明白如何判断XO2 和 XO3 的哪两个解在圆内，从几何构图看两个解都可以在外接圆内，为什么按照你的方程，我用Mathematica求解，比你的结果复杂得多?

    代入一组数字看看呗，就知道哪个解要保留，哪个要舍弃。至于结果，我是用 a1, a2 代替了两个根式，所以看起来好像简单。

denglongshan

准备就泰博定理等一些问题请教张院士，你看，还有其它问题吗？[br][br]-=-=-=-=- 以下内容由 denglongshan 在 时添加 -=-=-=-=-
其它与机器证明有关的问题，其它网友也可以提出。

天山草

下面引用由denglongshan在 2013/11/25 09:46pm 发表的内容：
准备就泰博定理等一些问题请教张院士，你看，还有其它问题吗？

咦，那好。我有好些问题，需要准备一下。

天山草

[这个贴子最后由天山草在 2013/11/27 05:18pm 第 1 次编辑]

先问几个想到的问题：
【1】运行程序时，开机运行时间 t1 为什么远大于开机后的第二次运行时间 t2 ？应该以哪次运行时间为准？
【2】程序的可读性，是指程序本身容易看得懂，还是运行结果容易看得懂，还是二者兼而有之？
【3】程序运行是以 mathematica 为平台的，目前这个平台对于较复杂的代数式处理能力还有限，可否代入具体数据进行“证明”？
【4】以泰博定理问题为例，AD 两侧的相切圆圆心坐标如果事先经过推导给出了表达式，在证明中可否直接引用？是否还需要对那个表达式的推导过程进行说明，甚至对结果的正确性加以证明？
【5】张院士在泰博定理的证明中，是如何确定那两个相切圆圆心坐标的？是利用其已有的“复数证明器”就可以呢，还是另有它途？

天山草

看了看唐灵推荐的一篇英文论文，认为【泰博定理】有以下内容：
（其中下图左的几个三点共线，前面已验证。图右的验证还没有做）

denglongshan

   不确定他是否会回信，以前写过一封，他回信了，把你的全部问题准备好。准备把我的程序给他，假如你认为有必要，也可以把你的程序一同发过来。五圆定理中，我认为最后证明角相等时，他的论文没有计算数据，应该是一个缺陷。
   你的第二个问题，你赞成我前面的意见吗？

天山草

[这个贴子最后由天山草在 2013/11/27 00:54pm 第 6 次编辑]

下面引用由denglongshan在 2013/11/26 10:37pm 发表的内容：
不确定他是否会回信，以前写过一封，他回信了，把你的全部问题准备好。准备把我的程序给他，假如你认为有必要，也可以把你的程序一同发过来。五圆定理中，我认为最后证明角相等时，他的论文没有计算数据，应该是 ...

也许张更愿意回到电脑邮箱，如果他对打字熟练的话。因此你要把你的邮箱地址给他。
张的五圆定理论文，角度结果也许是比较复杂，他在程序中有输出，但论文中省了。
我认为，电脑的机械化证明与传统证明有很大差异，其“可读性”包括对程序设计的思路要了解，但不必对程序语言很懂。因此程序中写明白注解是很有必要的，读者看程序，主要是看那些注解。
   如有可能，可以请张景中看看下面这个关于泰博定理的验证程序，如何才能变成证明程序；还是此路不通，不要继续走了：

denglongshan

我有张院士的电子信箱，论文中也有，你注意一下。几年前我写信给他还是用信封，由于告诉他我的邮箱，他给我是回电子邮件。
“电脑的机械化证明与传统证明有很大差异，其“可读性”包括对程序设计的思路要了解，但不必对很懂。”
可读的机器证明与传统证明本质一样，就是容易读懂的意思。只要输出结果容易看懂就行，没有必要理解程序语言和设计思路。
现在上传一篇例证法证明的论文，希望对你证明泰博定理有帮助。
你还可以与上面论文的作者联系。