明理创新实验室|AI4Math科研创新团队一论文获奖

多客科技

作者：微信文章
AI4Math

7月18日，明理书院AI4Math科研创新团队成员的论文《Learning an effective Premise Retrieval Model for Efficient Mathematical Formalization》被ICML 2025 AI For Math Workshop 接收，并获最佳论文提名奖。数学学院学生陶亦成与高瓴人工智能学院学生刘浩甜共同为论文一作，数学学院副教授王善文、高瓴人工智能学院长聘副教授许洪腾为论文指导教师。





自2023年成立以来，明理书院AI4Math科研创新团队汇聚了来自数学学院、统计学院和外国语学院等全校多个学院的优秀力量，形成了一支横跨文理的创新共同体。团队成员致力于探索利用人工智能推动数学形式化和定理证明的发展，进一步提高定理证明的效率和准确性，帮助验证一些相关数学领域中的关键定理证明；同时，以数学形式化的数学证明作为训练数据，提升人工智能的数理逻辑推理能力，在“AI赋能数学”与“数学反哺AI”的双向探索中不断前行。

秉持服务初心，团队让数学形式化这一领域走出实验室，成为赋能教与学的“通用语言”，让科技之花在服务中绽放。一方面，团队通过日常科普活动、大中协同育人项目，开展学科宣讲、数学形式化工作坊等活动推广形式化数学，帮助同学们掌握使用交互式证明助手Lean来学习数学，锻炼严谨的逻辑思维。另一方面，团队成员利用业余时间深入探究不同层次学习者使用Lean时遇到的困难，积极参与国际交流，向领域专家请教学习。针对实践中发现的实际困难，专注开发降低Lean教学门槛的工具以及适用于自学的Lean课件。









值得一提的是，除了此次获奖的Lean State Search搜索引擎，以陶亦成为核心成员的开发小分队，还开发了可支撑课程教学的Lean在线编辑器和课程网站。该课程网站支持自然语言和Lean语言提交，具备助教在线作业批改、学情分析、考试等功能。在今年7月暑期学校课程《代数与形式化数学》中已成功投入使用，发挥了重要作用。

此次获奖的 Lean State Search 搜索引擎，正是团队结合实践需求、攻克技术难关的重要成果。系列工具与平台的研发应用，也彰显了团队将科技创新融入教育领域，助力提升教学效率与学习效果的不懈追求。

来源｜AI4Math科研创新团队
审核｜许王莉 王善文