计算机验证后的欧几里得
Euclid After Computer Proof-checking
摘要：
欧几里德开创了一种数学理论的概念，这种理论是通过一系列合理的证明步骤从公理发展而来的。从一开始就有批评者和改进者。在本世纪，使用计算机来检查证明的正确性为严格性设定了新的标准。欧几里德如何在这样的检验下站得住脚呢？这个练习在几何学、数学基础以及逻辑与真理的关系方面能教给我们什么呢？
英文摘要：
Euclid pioneered the concept of a mathematical theory developed from axioms by a series of justified proof steps. From the outset there were critics and improvers. In this century the use of computers to check proofs for correctness sets a new standard of rigor. How does Euclid stand up under such an examination? And what does the exercise have to teach us about geometry, mathematical foundations, and the relation of logic to truth?
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
