该研究提出几何形式化理论GFT，构建兼容的平面几何形式系统，开发了包含88个谓词、196个定理的FormalGeo及求解器FGPS，可表示、验证并解决IMO级几何问题。团队标注了含6981个完整形式化问题的FormalGeo7k数据集，增强后达186832个。实验表明GFT正确实用，后向深度优先搜索失败率仅2.42%，结合深度学习可进一步降低。

本文介绍平面几何形式系统FormalGeo，包含88个谓词和196个定理，可表示、验证并解决IMO级几何题。配套FGPS求解器支持前后向搜索与AI辅助，FormalGeo7k数据集含6981题，后向搜索失败率仅2.42%。系统实现AI与形式推理结合，证明可读可验证，推动可解释几何自动推理发展。