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

💡提升AI的数学能力（AI4Math）不仅在智力上极具吸引力，而且对AI驱动的系统设计与验证至关重要。

🤖报告将重点讨论形式化数学推理，即通过Lean等形式系统来验证推理的正确性并提供自动反馈，这是一种与自然语言处理（NLP）互补的技术路径。

✅形式化数学推理有望帮助AI在数学、形式化验证以及可验证的代码生成等任务中取得重大进展。

📚报告嘉宾杨凯峪将介绍利用机器学习（特别是大型语言模型）处理两项关键子任务：定理证明（从定理陈述生成形式化证明）和自动形式化（将非形式化的数学转化为形式化数学）。