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