E老师：数学家的结论正确吗？

denglongshan

50年代，塔斯基用代数方法证明了初等几何的机械化的可能性。但是，我发现，即使象两内角平分线相等的三角形是等腰三角形也很难证明，更别提彭色列闭合定理多边形情形。以下内容摘自百度百科。
机器证明 编辑
本词条缺少名片图，补充相关内容使词条更完整，还能快速升级，赶紧来编辑吧！
机器证明及其应用是中国攀登计划项目之一。该项目的核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。
中文名 机器证明 简    介 机器证明及其应用是中国攀登计划 词    性 名词 分    类 计划
目录
1 基本简介
2 发展现状
3 展望与建议
基本简介编辑
实际上，机器证明研究领域的范围要广泛得多。在国外则更一般地叫做自动推理。我们把几何定理机器证明和非线性代数方程组作为主攻方向，一方面是因为吴文俊先生在70年代的突出工作，使中国在此方向上具有了领先的优势；另一方面，这两个方向有鲜明的应用背景，近年来在机器证明领域也确是十分活跃的，值得重视。由于传统的兴趣和多种原因，几何定理的机器证明在自动推理的研究中占有重要的地位。
发展现状编辑
近20年来，几何定理机器证明的研究和实践有了很大的进展。
从古老的梦想到惊人的突破
能否建立一个通用的几何解题方法，成批地解决问题，以至万理一证，是历史上一些卓越科学家的梦想。为此，笛卡尔发明了坐标系；莱布尼兹设想过推理机器；希尔伯特在其名著（几何基础）中给出了一类几何命题的机械化定理。电子计算机的出现推动了数学机械化。50年代，塔斯基用代数方法证明了初等几何的机械化的可能性。到60年代，斯拉格和莫色斯实现了符号积分，代数与分析计算问题的机械化已经初具规模，而几何定理的机器证明看来仍遥遥无期。接着，格兰特等提出用逻辑方法建立几何推理机，科林斯等改进了塔斯基的代数方法。直到1975年，仍找不到能用计算机判定非平凡几何命题的有效算法。正当这一领域的热情由于进展缓慢而趋于冷落之际，吴文俊方法的提出给定理机器证明的研究带来勃勃生机。用吴法可在微机上很快地证明困难的几何定理。周咸青发展了吴法并把它实现为有效的通用程序，证明了512条非平凡定理，写成英文专著。这一进展是自动推理领域的一大突破，被国际同行誉为革命性的工作。
从机器判定到可读证明的自动生成
吴法的成功使一度冷落的几何定理机器证明研究活跃起来。用代数方法证明几何定理的方向受到重视。新的代数方法接连出现。在国外，周咸青等提出了用Grobner基方法构作几何定理机器证明的算法和程序并获得成功。在国内，洪家威提出了单点例证方法的理论设想，但因复杂度太大不能实现。张景中、杨路则提出数值并行方法，在低档微机（甚至计算器）上实现了非平凡几何定理的机器证明和机器发明。数值并行方法的优点是所需内存极小，且易于并行化。所有这些方法都属于代数方法。它们的提出和实现丰富了几何定理机器证明的研究。但与吴法相比，没有大的新突破。代数方法不能使人满意的是，它所给出的"证明"是关于大多项式的繁复的计算，人难于理解其几何意义,也难于检验其是否正确。能否让计算机生成人能理解和易于检验的简明巧妙的证明，即所谓可读证明，是对自动推理和人工智能领域的一个挑战性的课题。一些著名的科学家认为，机器证明的基本思想是以量的复杂取代质的困难，这就很难想象用机器生成可读证明。国外一些学者从60年代即致力于几何定理可读证明自动生成的研究，30多年来进展不大，未能给出哪怕是一小类非平凡几何定理的机器证明的有效算法和程序。作者以多年来所发展的几何新方法为基本工具，并提出了消点思想，和周咸青、高小山合作，于1992年突破了这一困难，实现了几何定理可读证明的自动生成。这一新方法既不以坐标为基础，也不同于传统的综合方法，而是一个以几何不变量为工具，把几何、代数、逻辑和人工智能方法结合起来所形成的开放系统。它选择几个基本的几何不变量和一套作图规则，并且建立一系列与这些不变量和作图规则有关的消点公式。当命题的前提以作图语句的形式输入时，程序可调用适当的消点公式把结论中的约束点逐个消去，最后达到水落石出。消点的过程纪录与消点公式相结合，就是一个具有几何意义的证明。此算法对可构造等式型几何命题是完全的，但其应用范围不限于这一类命题。基于此法所编的程序，已在微机上对数以百计的困难的几何定理完全自动地生成了简短的可读证明，其效率也比其他方法为高。随所用的几何量的不同，它能生成面积法、向量法、复数法和全角法等多种风格的证明，也能用于立体几何。杨路、高小山、周咸青与作者合作，把消点法用于非欧几何可读证明的自动生成也获得成功，并得到一批非欧几何新定理。消点法也可用于几何计算和公式推导。基于几何量和消点思想的新原理的建立，像是打开了几何定理机器求解的一个矿床。它也使几何定理机器证明的成果在数学教育中的应用有了现实可能。这一成果被国际同行誉为使计算机能像处理算术那样处理几何的发展道路上的里程碑，是自动推理领域30年来最重要的工作。在多数情形下，消点法也可用笔纸证明不平凡的定理。它结束了两千年来几何证题无定法的局面，把初等几何解题法从四则杂题的层次推进到代数方程的阶段。
机器证明与人工证明媲美的新阶段
但是，比起人类在几千年间积累起来的丰富多彩的几何知识来，计算机目前所能做的仍是十分有限。应当把几何学家所掌握的方法更多地"教给"计算机，使计算机产生的解法可以与几何学家相比。为此，要分析几何学家有哪些解题方法，计算机已经学会了哪些，以确定下一步应当做什么和如何做。
几何学家常用下列四种手段：
W1.检验：对具体图形作观察和计算，以确信命题为真；
W2.搜索：依据常用的引理和已知条件去找寻题图中更多的几何性质。这样做如达不到目的，得到的信息就是进一步工作的基础；
W3.归约：从结论出发，利用已知信息消去依赖的几何量或几何元素，使结论的真假趋于显然或易于检验；
W4.转化：改变命题的形式，如几何变换、反证法、辅助线等。
手段W1的机器模拟已经实现。手段W3的机械化研究得到了最大的成功。吴法、GB法、面积法和向量法均属此类。手段W4充分体现了人的思维活动的灵活性与丰富性，尚难以机械化。手段W2，搜索，是传统几何证明活动中的常规方法，是归约的补充和转化的基础。
我们基于前推模式设计并实现了一个"几何信息搜索系统"(GISS）。由于适当选择几何工具，合理组织数据和优化推理的过程，效果极好。文献中曾提出的用搜索法处理涉及圆的命题，以及找出所有可能推出的几何性质（达到推理不动点）的问题，均被我们的算法完满回答。我们的程序用C语言在NeXT工作站上实现，用于161个非平凡几何命题，均在合理的时间内达到不动点，并能发现新定理，证得其它方法不能证明的结果。程序已具有添加某些辅助线的功能。
非线性代数方程组的研究
机器生成可读证明的实现并不使代数方法失去价值。一些特殊问题及代数曲线、曲面的几何问题仍需用代数方法求解。代数方法与非线性代数方程组的理论和符号求解密切相关，有广泛应用，是自动推理的一大热点。数学、物理和工程技术中的许多问题，归根结底要靠解代数方程组。线性方程组还好办，非线性方程组就成了难关。特别是非线性方程组的符号求解，更难，理论上也更重要。对非线性代数方程组的研究，19世纪就提出了各种结式方法。由于结式法涉及大行列式的计算，算不动，研究就冷下来。本世纪有了计算机，人们又研究新的算法。在60年代，国外提出GB法和Ritt法。GB方法是完全方法。Ritt方法经吴文俊先生改进后，也成了一种完全方法。叫Ritt-Wu方法,在中国简称吴法（把Ritt-Wu方法用于几何定理的机器证明，也叫吴法。国外有人把机器证明的吴法叫Ritt-Wu方法，是不确切的。Ritt和几何定理机器证明没有关系）。两个方法哪个更好，目前还没有定论。用于几何定理机器证明，吴法确实比GB法强。中国学者还用吴法解决了许多重要问题，涉及理论物理、微分方程、样条理论和机器人。虽已有了吴法、GB法等优秀的完全方法，但是道高一尺，魔高一丈，更难的问题要求更有力的新方法。
近年来，国外一再提出新的思路和算法，欧共体还投资数百万美元组织项目专门研究非线性代数方程组的解法，但均无突破性进展。最近，基于我们提出并加以完善的新的理论和算法———结式矩阵法，符红光编写了代数方程组符号求解和机器证明的MAPLE程序。新算法的特点是：
⑴是非线性代数方程组符号求解和相容性判定的完全方法。
⑵不依赖于多项式的因式分解。
⑶用我们提出的弱非退化条件作零点分解，减少多余分支。
⑷子结式计算与数值检验配合，进行大范围消元。
⑸将所给方程组分解为三角列，便于机器证明和最终求解。
经许多例子的演算，它比已知的各种方法有更好的效果。此法能在PC486机上解六变量循环方程，反解各种类型的六关节机器人问题，这是其它方法做不到的。非线性代数方程组研究的又一新进展是杨路等提出的实系数代数方程的判别式系统。这不但彻底解决了几世纪悬而未决的关于代数方程一个基本问题，也使几何不等式机器证明的难题得到了突破。杨路等最近所写的程序，能快速地证明许多几何不等式，根据已给条件推出几何不等式，并已改正和改进了国外一些关于几何不等式的结果。
展望与建议编辑
预计在未来十年中初等几何等式型问题的机器求解将基本完成，并进入实用阶段。在前述成果的基础上，会出现新的热点：
⑴在几何定理可读证明自动生成工作的影响下，用几何不变量为工具进行机器求解的研究会有新的进展。例如几何作图的机器求解，几何推理数据库的研究及微分几何可读证明的研究。
⑵几何不等式的机器求解，会随着实代数研究的进展而出现新的突破。
⑶非线性代数方程组的理论与算法，仍将是热点。结式法和插值方法等利于并行的算法会得到更多重视。
⑷微分多项式的机器推导研究将得到开展。
⑸机器证明的成果，特别是非线性代数方程组理论与算法的研究成果，将在数学、物理和工程技术中得到更多的应用。目前,在几何定理机器证明方面，中国处于国际领先地位。
在非线性代数方程组研究领域，竞争激烈，中国已进入先进行列，但还不能说领先。在数学机械化软件开发方面，由于起步晚、队伍小和资金不足等原因，中国远不及欧美先进国家。我们不应满足于某些方向上的领先地位。在继续进行几何定理机器证明研究并保持领先的同时，要把力量集中到非线性代数方程组的方向上来，特别应加强对实用而有效的算法的研究。在数学机械化推广应用方面，也应投入力量，发挥我们在理论与算法方向的优势，在软件开发方面赶超先进。在几何定理机器证明成果的基础上，开发高智能的教育软件和自主版权的符号演算数学软件，为中国科技、教育事业作出贡献。
（此文是作者在中国计算机学会第九次全国学术会议上所作的特约报告的详细摘要）

elim

我们这个论坛软件对一些 ascii 符号不能正确显示：

首先看看什么叫证明。举一个例子：

幺元定义：∀ a  ∈ ℝ (1a = a)∧(0 + a = a)∧(1 ≠ 0)

在实数公理中有以下几条：
逆元公理 ∀ a  ∈ℝ ∃ -a ∈ ℝ (a +(-a) = 0)
               ∀ a  ∈ℝ -{0}  ∃ a^{-1} ∈ℝ (a a^{-1}= 1)

由上得：-a = 0 +(-a) = ((-1)+1)a + (-a) = (-1)a +a+(-a) = (-1)a
              (-1)^2 = (-1)^2+(-1)+1=(-1)(-1+1)+1=1
              (-a)^2 = (-1)^2 a^2 = 1 a^2 = a^2

三歧性： &#8704;a, b  ∈&#8477; ((a=b)∨(a>b)∨(a<b))
保序性： &#8704; a, b, c ∈&#8477; ((a > b) &#8658; (a + c > b + c))
               &#8704; a, b, c ∈&#8477; ((a > b)∧(c > 0) &#8658; (ac > bc ))

进而        (a ≠ 0) &#8660; ((a > 0) ∨ (0 > a)) &#8658; (a^2 > 0)∨(-a > 0)
               &#8658; (a^2 > 0)∨((-a)^2 > 0) &#8658; a^2 > 0

推论：    1 = 1^2 > 0

命题是合式公式，定理是被证明了的命题，
证明是从公理或已知定理到待证命题的有限逻辑蕴含序列。

由此不难知道可证命题的机器证明总是存在的。但完能的
机器证明方法是不存在的，因为不是所有命题都是可判定
的。

随着技术的发展，机器证明很可能胜过大多数人工证明。

虽然机器证明会日益强大，但机器没有真正意义上的理解
和审美，所以对机器是否有能力在茫茫的定理海洋中确立
什么是可点可圈的定理，什么是不值多提的命题，很值得
怀疑。

denglongshan

谢谢老师，可惜不懂

elim

塔斯基用代数方法证明了初等几何的机械化的可能性。

塔斯基是搞元数学的。他的证明一定诉诸于数理逻辑，命题演算。建议你学习一下数理逻辑。

elim

二楼的一点注释：
幺元定义： 加法幺元是 0， 乘法幺元是 1， 两者不等，且对每个 a 有 0+a = a, 1a = a.
作为习题，试证在数域中 加法幺元，乘法幺元是唯一的。

假定 0，0* 都是加法幺元, 那么由幺元定义,  0* = 0+0* 且 0*+0 = 0.  由交换律得 0* = 0.
类似地可证乘法幺元的唯一性.
由于 0a + a = 0a +1a = (0+1)a = (1) a = 1a = a 对一切 a 成立
(第一个等式根据乘法幺元的定义，等式2是乘法对加法的分配律，
等式3由加法幺元的定义得到，接着由乘法幺元的定义得到最后的等式)
现在再根据加法幺元的定义及唯一性，就证明了  0a = 0.
我们一直以为 -a = (-1)a 是天经地义的，但“认为”不等于证明。所以给出以下证明：
对任意 a, 由逆元公理，存在 -a 使得 a + (-a) = 0.  由加法幺元的定义，我们有
-a = (-a)+ 0 = (-a) + (1+(-1))a = ((-a)+a) +(-1)a = 0 +(-1)a = (-1)a
网友可以补足上面的各等号成立的理由. 重要的是了解，我们所确立的一切算术公式
都可从数域公理，定义推出。不需要任何想当然，或者“无需证明”之类的瞒天过海。

elim

注意实数域公理只假定 1 不是 0，三歧性以及算术的有条件的保序性。
二楼的其余部分旨在证明 a^2 = (-a)^2 > 0, 及其推论 1 > 0.

相信我给出的证明的例子使大家了解到通常意义下所谓的算术的机器可证性。
由于几何可以完全地算术化，这就大概给出了塔斯基的论断的解读。

elim

研究机器证明而不了解数理逻辑，命题演算和公理化方法，是不可想象的，没有希望的。

顺便提一下 jzkyllcjl，他的数学主张毫无建树，为人类所不齿的原因，正是在于他不了解数学的本质在于对具体的量的量纲及测不准性的扬弃。他的所谓实践，本质上是丧失实践和理论能力的实践。所以他的一辈子的“努力”只能血本无归。

denglongshan

在这里没有提他，那你认为我的论文有问题吗？搜狗百科关于 彭赛列闭合定理的介绍的开头部分：彭赛列闭合定理
编辑词条

平面上给定两条圆锥曲线，若存在一封闭多边形外切其中一条圆锥曲线且内接另一条圆锥曲线，则此封闭多边形内接的圆锥曲线上每一个点都是满足这样（切、接）性质的封闭多边形的顶点，且所有满足此性质的封闭多边形的边数相同。
最简明的彭赛列闭合定理表示为：一个三角形外接于一个圆，内切一个圆，则外接圆可以有无数个内接三角形满足其内切圆为上述的同一个。
彭赛列闭合定理展示了基于圆锥曲线关系上的一种“群结构”（group structure）关系——“彭赛列结构”（Poncelet type），表示为：有一个满一种结构的关系存在，则所有都满足这种结构的关系都存在，可以扩展为更为高维的概念，彭赛列闭合定理只是这种结构关系的其中一种。

谢谢老师指导，高中程度能否理解？现在事务繁多，没有太多精力学习。

denglongshan

所谓机器证明的一个最重要方法，就是把几何条件和结论转换成代数表达式，从条件表达式可以推出结论表达式，很遗憾，一些问题出现高次方程，很难解释计算结果或算不出来。

elim

对应于高次方程的问题的确头痛。但定性分析应该是可以的。总的说来，技术上的难处不能定性地推翻机器证明一般的可行性。