【摘要】：机器定理证明，是人工智能领域中的一个重要分支，是数学、计算机科学的一门交叉学科。机器证明及其应用，是我国攀登计划项目之一。项目核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。几何定理机器证明的基本原理 图片来源：当当网吴文俊老师上课场景实际上，机器定理证明的梦想很久以前就开始萌芽。同一时期，我国数学家吴文俊提出了“吴方法”。机器定理证明一直在行走，并最终会造福世界。
机器定理证明，是人工智能领域中的一个重要分支，是数学、计算机科学的一门交叉学科。顾名思义，简单来说，是利用机器通过类似于人类的演绎推理、代数运算等，利用已知条件证明相应结论。机器证明及其应用，是我国攀登计划项目之一。项目核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。实际上，机器证明研究领域的范围要广泛得多。我国将这二者作为主攻，一方面得益于吴文俊先生在70年代的突出工作，另一方面，这两个方向具有鲜明的应用背景。
几何定理机器证明的基本原理（初等几何部分）
图片来源：当当网
吴文俊老师上课场景(www.xing528.com)
实际上，机器定理证明的梦想很久以前就开始萌芽。以几何为例，能否建立一个通用的几何解题方法，成批地解决问题，以至万理一证，是历史上一些卓越的科学家的梦想。为此，笛卡尔发明了坐标系，莱布尼兹设想过推理机器，希尔伯特在其名著《几何基础》中给出了一类几何命题的机械化定理。之后，电子计算机的出现推动了数学机械化。50年代，初等几何的机械化的可能性被证明。60年代，实现了符号积分。70年代，几名数学家以计算机为辅助证明了困扰人们许久的“四色猜想”（从而变为“四色定理”）。同一时期，我国数学家吴文俊提出了“吴方法”。90年代，几何定理可读性证明取得突破性进展。机器定理证明一直在行走，并最终会造福世界。
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
