通过勤奋努力和坚定承诺，研究人员踏上了一项多年的旅程，创建了一个全面的形式平面几何系统，以弥合困难的IMO级问题和AI自动推理之间的差距。这个形式系统允许现代AI模型以人类可读、可追溯和可验证的方式推导复杂几何问题的解决方案。他们的研究引入了几何形式化理论（GFT）来指导系统开发，其中包括几何谓词和定理的FormalGeo。它还提供了用于AI集成的基于Python的FGPS（Formal Geometry Problem Solver）和注释的FormalGeo7k数据集。文章讨论了AI作为解析器和求解器的角色，强调了系统的正确性和实用性，并提出了通过深度学习技术可能的改进。
在几何问题解决中，已经提出了各种方法，包括Gelernter的后向搜索、Nevins的前向链接、吴的代数方法和张的点消除方法。已经创建了几个形式系统和数据集，但往往需要更多的理论指导和可扩展性。CL模型、SCA和GeoDRL等AI辅助系统旨在提高成功率。代数方法和数值并行方法也做出了重要贡献。共享基准和数据集推动了AI辅助几何问题求解的研究。
数学和计算在互为益处的关系中分享，计算既能够促进数学工作，也为形式数学提供了一个平台。人工智能的出现扩展了计算机辅助数学问题解决的可能性。斯坦福大学2021年AI100报告强调了IMO大挑战，寻求一个能够为形式问题生成机器可检验证明并在国际数学奥林匹兽数学方面取得优秀成绩的AI系统，强调了全面数学形式化的需要。虽然在机械化数学问题方面已经取得了进展，但几何问题的形式化和机械求解面临挑战，如一致性知识表示和难以读取的过程。
这项研究引入了一个全面的平面几何系统FormalGeo，包括几何谓词和定理。它提出了一个基于Python的几何问题求解器FGPS，提供交互式辅助和自动求解。为几何问题进行了正式语言注释的FormalGeo7k数据集有助于AI集成。该研究将现代AI模型与系统对齐，以实现对具有挑战性的几何问题的演绎推理。它提出了用于系统开发的GFT，并采用GDL和CDL进行问题定义。后向深度优先搜索方法显示出低失败率，并且可以通过深度学习技术进行进一步改进。
FormalGeo是一个全面的正式平面几何系统，包括88个谓词和196个定理，可以验证和解决具有挑战性的几何问题。FGPS是一个基于Python的问题求解器，提供交互式辅助和自动求解方法。FormalGeo7k数据集是一个具有正式注释的几何问题数据集，有助于AI集成。现代AI模型增强了系统，产生了可读、可追溯和可验证的证明。实验证实了GFT，并且FGPS的后向深度优先搜索方法实现了低2.42%的错误率，具有通过深度学习技术进一步提升的潜力。
该方法引入了GFT指导几何问题形式化，并提出了FormalGeo系统和FGPS求解器。通过对FormalGeo7k数据集的实验验证了GFT，使用后向深度优先搜索方法的错误率只有低2.42%。进一步的改进包括扩展谓词、对IMO级数据集进行注释以及实施深度学习技术。现代AI集成使得AI能够提供可读、可追溯和可验证的几何问题解决方案。FormalGeo7k数据集和FGPS源代码的提供促进了自动几何推理的进一步研究和开发。