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

本文综述几何自动推理领域进展，涵盖GeoGebra Discovery新增ShowProof命令（输出证明步骤与难度评分）、统一基准UniGeo及Geoformer模型、GeoTutor辅导系统、Inter-GPS求解器、FormalGeo形式系统与FGPS、GeoQA数据集、视觉语言模型几何推理评估以及ADG 2023会议。