摘要：本讲座将深度解析大语言模型在数学领域从“竞赛解题”到“科研协作者”的演进历程。我们将回顾 NuminaMath、Qwen、OpenAI o1、DeepSeek R1 及 Gemini DeepThink 在非形式化推理上的范式革命，并结合 DeepSeek-Prover 与 Seed-Prover 等前沿工作，探讨如何利用 Lean 等形式化语言（Formal Math） 构建自动验证体系，从根本上解决大模型的幻觉问题。最后，讲座将展望 AGI 视角下数学科研的新未来，分析 AI 如何重塑数学家的工作流，并为学生在 AI 时代如何平衡数学逻辑与编程技能提供实质性建议。

主讲人介绍：Project Numina的创始人，前Cardiologs的创始人兼CTO。Project Numina是一个开源的致力于促进AI在数学领域发展的组织，其数学大模型赢得了AIMO委员会设立的第一届AIMO progress prize，后续也开源出了NuminaMath 数据集和Kimina prover 等一系列的工作。