ByteDance（字节跳动）

Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Euclean：在Lean中通过统一验证实现几何问题的自动形式化

Linbin Tang, Jingyan You, Zilin Kang, Hanzhang Liu, Sophia Zhang, Zenan Li, Chenrui Cao, Liangcheng Song, Jiaao Wu, Xian Zhang, Fan Yang

机构 * Google DeepMind（谷歌DeepMind） ； ByteDance Seed Team（字节跳动种子团队） 纠错

AI总结 研究针对几何问题形式化的碎片化现状，提出Euclean框架，通过四个阶段在Mathlib中自动形式化几何，构建了大型数据集，经评估有一定准确率，能提升Goedel v2证明成功率，验证了数据集质量。

Comments ICML 2026