This is the first paper in a series of work we have accomplished over the past three years. In this paper, 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，我们建立了FormalGeo系统，包含88个几何谓词和196个定理，能够表示、验证和解决IMO级几何问题。我们还用Python开发了FGPS（形式几何问题求解器），既可作为验证解题过程的交互式助手，也能通过前向搜索、后向搜索及AI辅助搜索等多种方法实现自动求解。我们标注了FormalGeo7k数据集，包含6,981个（通过数据增强扩展至186,832个）带有完整形式化语言标注的几何问题。形式系统的实现及在FormalGeo7k上的实验验证了GFT的正确性和实用性。后向深度优先搜索方法的解题失败率仅为2.42%，且我们可通过融入深度学习技术实现更低失败率。FGPS源代码和FormalGeo7k数据集已开源：https://github.com/BitSecret/FormalGeo。