定理机器验证是自动推理领域内的一个重要研究课题，其研究方法和研究成果具有十分显著的理论意义与应用价值。目前研究者们已成功验证了数学中一些较为复杂的定理和猜想问题，例如四色定理、Kepler猜想以及李群8 E结构等。这些工作不仅推动了数学领域中定理机器验证的研究，也对其他领域定理的研究提供了有利的帮助。　　有限几何定理由于点线关联结构复杂多样化的特点引起了研究者们的关注。目前，研究者们已编写出一些验证有限几何定理的计算机程序，但这些程序运行时间较长，可读性较差，同时程序的语法相对繁琐复杂，不易于理解，导致研究者们关于这些程序的研究并无太大进展，致使有限几何定理的机器验证也无较大的发展。本文提出利用Alloy验证有限几何定理的新方法。该方法的的优点是：语言精练简洁，易于理解，表达能力较强，程序相对简单，同时验证效率较高，验证结果可读性较好。　　本文对有限几何中的n阶射影平面存在性定理和n阶仿射平面存在性定理进行了机器验证。基本步骤为首先用Alloy建模语言对这两类定理进行建模，然后借助于Alloy分析器对模型进行自动化分析。验证结果表明，该方法不仅效率高，而且可读性较强，同时还能够给出具体平面存在的可视化实例。本文提出的方法为我们研究有限几何定理中结构较为复杂的开问题提供了一个新的验证思路。