题目：AI for Mathematics：数学的数字化与智能化

报告人：董彬教授（北京大学国际数学研究中心）

摘要：本报告将重点关注近年来人工智能在辅助数学探索中的一些进展。首先，我将回顾人工智能与数学在历史发展中是如何相辅相成，特别是人工智能和数学双向赋能的重要性。其次，我将介绍目前正在进行的一些工作的初步成果，包括通过对数学的数字化来构建高质量的数学数据集，以及后续的智能化的设想。最后，我们将展望人工智能与数学交叉研究领域的未来机遇与挑战。

报告时间：2025年5月10日上午9：30-10：30

报告地点：教二楼113

题目：Lean语言形式化定理证明初探

报告人：姜杰东博士（北京大学）

摘要：Lean 是一个强大的交互式定理证明工具，既能用于数学形式化验证，也能帮助初学者以编程的方式理解严谨的逻辑推理。我们将通过大量现场演示，展示如何用 Lean 编写定义、陈述定理并完成证明，同时初步介绍其核心语法和交互式逻辑。此外，报告将重点推荐适合入门的互动学习游戏 Natural Number Games——这是一款通过游戏化关卡介绍Lean的教学游戏，无需前置知识即可轻松上手。相关链接：

Lean社群官方主页：https://leanprover-community.github.io

报告时间：2025年5月10日上午11：00-12：00

报告地点：教二楼113