人工智能是一门研究模拟和延伸人的智能的一门新技术科学[1]。它作为计算机科学的一个分支,旨在了解智能的实质,并生产出一种新的能模拟人类智能的方式进行思考并作出决策行动的智能机器,该领域的研究包括机器人、语言识别、图像识别、自然语言处理和专家系统等。人工智能从诞生以来,其理论和技术日益成熟,应用领域也不断扩大。人工智能在数学机械化领域的突出体现就是机器证明。机器证明是通过计算机和辅助证明工具实现定理证明的一门学科。目前的辅助证明工具有Coq、Isabelle、HOL Light等。Coq是目前国际上最主流的辅助证明工具之一,它起源于法国,其核心是归纳构造演算,这也使得Coq拥有了很强的严谨性与可靠性。不仅如此,Coq交互式的证明环境也给使用者带来了极大的便利。目前,人们利用Coq已经证明了许多著名的数学定理,其中最有影响力的是Gonthier和Werner在2005年完成的“四色定理”的机器证明。在这之后,2012年Gonthier又给出了有限单群分类定理的机器验证,到了 2015年Hales等人又完成了 Kepler猜想的计算机证明。这些成果使得辅助证明工具Coq在学术界的影响日益增强。初等几何是数学领域的一个重要研究课题,自从欧几里得创立初等几何以来,几何学的发展就离不开初等几何,之后的射影几何、非欧几何等都是在初等几何的基础上发展过来的。杨路定理是由我国著名数学家杨路先生提出的一个初等几何定理,杨路定理作为开普勒定理的一个扩展,现已被收录进日本岩田志康先生所编纂的《几何学大辞典》中,是非常具有代表性的一个定理,在海外也拥有着不俗的影响。在对杨路定理进行形式化证明的前期准备中,我们不仅可以构建出一系列初等几何的概念,还可以引入坐标、向量等解析几何的概念,最后我们通过构建出来的概念和性质等对杨路定理进行描述和证明。本文借助辅助证明工具Coq,完成了点、线、面、角等初等几何概念和向量、坐标的构建。最后我们给出了杨路定理的完整描述与机器证明。本文的创新点在于利用交互式辅助证明工具Coq进行机器证明,并且这是杨路定理的首次形式化,是对于初等几何体系形式化搭建的一次尝试,将来我们可以在此基础上进行更多的尝试,发展出更多不同的几何体系。