8. 欧氏几何及其重要意义
数学是一棵富有生命力的大树，从它史前诞生之时起，就为自己的生存、发展而斗争。这场斗争经历了史前的几个世纪和随后有文字记载历史的几个世纪，最后终于在肥沃的希腊土壤中扎稳了生存的根基，并且在一个较短的时期里茁壮成长起来了。在这个时期，它绽出了一朵美丽之花——欧氏几何。其他的花蕾也含苞欲放。

欧几里德与《几何原本》

欧氏几何是数学中最古老的一个分支，也是数学中最基础的一个分支。欧氏几何经过了数千年的发展和积累，到了公元前三百年左右时，希腊大数学家欧几里德（Euclid，公元前300年前后）把零散、孤立、不系统的几何知识总结成一门具有比较严密理论体系的几何学，写出了数学巨著《几何原本》。

《几何原本》的伟大历史意义在于它用公理法建立起最早的数学演绎体系，在这个体系中有四方面的主要内容：定义、公理、命题、定理。在这部著作里，全部几何知识都是从最初的几个公理、运用逻辑推理的方法展开和叙述的。
这些公理、公设就是《几何原本》全书的基础。全书以这些公理和定义为依据，逻辑地展开它的各个部分。比如后面出现的每一个定理都写明什么是已知、什么是求证，都要根据前面的定义、公理、定理进行逻辑推理给予仔细证明。
从欧几里得发表《几何原本》到现在已有两千多年，尽管科学技术日新月异，但欧氏几何仍旧是中学生学习数学基础知识的好教材。长期以来，人们都认为《几何原本》是两千多年来传播几何知识的标准教科书，在西方是除了《圣经》以外销路最广的一本书。由于欧氏几何具有鲜明的直观性并和逻辑演绎方法密切相结合等特点，长期实践表明，它是培养、提高青少年逻辑思维能力的好教材，很多家长以此训练孩子的推理能力。历史上不知有多少科学家从欧氏几何学习中得到培养和训练，从而提高了科学研究的兴趣和能力及基础素质，为人类作出了伟大的贡献。此外，欧氏几何还具有高超的美学价值，随着几何学美妙结构和精确推理的发展，数学变成了一门艺术。
9. 几何定理计算机证明的方法
从数学众多分支角度上看，几何在数学中历史地位突出，在数学教育中的作用重要，因此对几何定理进行计算机证明成了数学定理证明领域中的研究重点，发展较快，成果众多。从理论和分析角度上看，用计算机自动证明某一类型几何定理，一般要经历公理化、坐标化与代数化、机械化等步骤，就能编制程序并在计算机上实现，条理清晰，用计算机进行几何定理证明较易实现。
现在，几何定理计算机证明的方法主要有以下三种：
一、代数方法
可用计算机证明的几何定理都假设坐标化与代数化已经完成，而且可把几何定理的证明问题化为一些代数关系式的处理问题，有三种不同类型，与之对应则有三种不同的计算机证明方法。
第一类，假设代数关系式对于变量是线性的，证明方法为希尔伯特方法；
第二类，假设代数关系式可用多项式的方程表示，证明方法是中国数学家吴文俊首先提出的，称为吴文俊方法，简称为吴方法；
第三类，假设代数关系式为多项式等式或不等式，但其系数必须在一实闭域中，证明方法为塔斯基方法。
这三种方法各有其适用范围，但就通用的定理证明来说，希尔伯特法效率较高而塔斯基法效率较低，但前者的适用范围很窄。
二、几何不变量消点法
以吴方法为代表的代数方法仅能够判断几何命题的成立与否，证明过程复杂，需要进行大量的数值计算和符号计算，与传统几何证明的简洁明了相差甚大。人们很难读懂这种方法生成的证明，因此很多人难以接受这种证明的风格。如何生成让人容易读懂的几何证明过程，成为科学家面临的又一个严峻的挑战。1992年，张景中院士以面积法为基础，提出了基于几何不变量的消点法。随后，他与周咸青、高小山合作完善了这个方法，利用计算机对大量非平凡的几何命题生成了简洁易读的几何证明。这一杰出的工作被誉为计算机处理几何问题的里程碑。
三、基于演绎数据库的搜索法
几何不变量的方法虽然实现了一大类几何定理机器证明的可读性，但是这种方法得到的证明过程常常不符合人的思维习惯。而利用演绎数据库的方法，根据几何命题所给的条件、已知的公理、定理及公式等推理规则，通过大量试验匹配的方法进行证明，得到从结论出发进行搜索的后推链方法。
随着几何定理计算机证明的进一步发展，还会有一些新的、更加有效和更易理解的证明方法出现。