This is the first article of our work over the past decade. In this series of papers, we have constructed a complete and compatible formal plane geometry system. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning. With this formal system in place, we have been able to seamlessly integrate modern AI models with our formal system. Within this formal framework, AI is now capable of providing deductive reasoning solutions to IMO-level plane geometry problems, just like handling other natural languages, and these proofs are readable, traceable, and verifiable. We propose the geometry formalization theory (GFT) to guide the development of the geometry formal system. Based on the GFT, we have established the FormalGeo, which consists of 88 geometric predicates and 196 theorems. It can represent, validate, and solve IMO-level geometry problems. we also have crafted the FGPS (formal geometry problem solver) in Python. It serves as both an interactive assistant for verifying problem-solving processes and an automated problem solver, utilizing various methods such as forward search, backward search and AI-assisted search. We've annotated the FormalGeo7k dataset, containing 6,981 (expand to 186,832 through data augmentation) geometry problems with complete formal language annotations. Implementation of the formal system and experiments on the FormalGeo7k validate the correctness and utility of the GFT. The backward depth-first search method only yields a 2.42% problem-solving failure rate, and we can incorporate deep learning techniques to achieve lower one. The source code of FGPS and FormalGeo7k dataset are available at https://github.com/BitSecret/FormalGeo.

翻译：本文是我们过去十年工作的首篇论文。在这系列研究中，我们构建了一个完整且兼容的形式化平面几何系统，这将为IMO级平面几何挑战与可读的AI自动推理之间架起关键桥梁。借助这一形式化系统，我们得以将现代AI模型与我们构建的形式化系统无缝集成。在此框架下，AI现在能够像处理其他自然语言一样，为IMO级平面几何问题提供演绎推理解决方案，且这些证明具有可读性、可追溯性和可验证性。我们提出几何形式化理论（GFT）以指导几何形式化系统的开发。基于GFT，我们建立了包含88个几何谓词和196个定理的FormalGeo，能够表示、验证并求解IMO级几何问题。我们还用Python开发了FGPS（形式化几何问题求解器），它既可作为验证解题过程的交互式辅助工具，也可通过前向搜索、后向搜索及AI辅助搜索等多种方法实现自动化求解。我们标注了包含6,981个（通过数据增强扩展至186,832个）具有完整形式化语言标注的几何问题的FormalGeo7k数据集。形式化系统的实现及在FormalGeo7k上的实验验证了GFT的正确性与实用性。后向深度优先搜索方法仅产生2.42%的解题失败率，且可通过引入深度学习技术进一步降低该指标。FGPS源代码与FormalGeo7k数据集已发布在https://github.com/BitSecret/FormalGeo。