本次报告聚焦于AI4Math，探讨如何提升AI的数学能力，这不仅具有智力吸引力，还在AI驱动的系统设计与验证中扮演关键角色。报告将介绍一种与NLP互补的技术路径：形式化数学推理，通过Lean等形式系统验证推理的正确性并提供自动反馈。形式化数学推理有望助力AI在数学、形式化验证和可验证代码生成等任务中取得进展。报告嘉宾杨凯峪将介绍利用机器学习处理定理证明和自动形式化两项关键子任务，并讨论形式化数学推理中的开放问题和关键里程碑。

💡AI4Math研究旨在提升人工智能的数学能力，这对于AI驱动的系统设计与验证至关重要，具有重要的研究价值和应用前景。

📚报告将探讨形式化数学推理这一技术路径，它与广泛借鉴NLP技术的传统方法互补，通过Lean等形式系统来验证推理的正确性并提供自动反馈，为AI数学能力的提升提供新的思路。

🤖报告嘉宾杨凯峪是Meta FAIR的研究科学家，他将介绍如何利用机器学习（特别是大型语言模型）处理定理证明（从定理陈述生成形式化证明）和自动形式化（将非形式化的数学转化为形式化数学）这两项关键子任务，并分享他在该领域的研究成果。

🚧报告还将讨论形式化数学推理中的开放问题和关键里程碑，为该领域未来的发展方向提供参考。