北京
导语
在2023年，由集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师共同发起“”读书会，希望从 AI for Math，Math for AI 两个方面深入探讨人工智能与数学的密切联系。我们也在持续关注这个领域的发展。
形式化数学推理代表了AI for Math的新前沿，它结合了数学的严谨性与AI的创造力。这种结合有希望开发出能够可靠地进行复杂数学推理的AI系统，这不仅会推动数学本身的发展，还会为科学、工程和技术领域带来变革性影响。我们特别邀请到北京国际数学研究中心徐天一研究员在本周三（3月12日）晚在读书会上做加餐分享，关于AI+形式化数学的话题，是什么、为什么以及怎么做。
AI for formalized math: What, why, and how?
分享流程
19:00-20:30 主题分享，主讲人：徐天一
20:30-21:00 圆桌讨论，嘉宾：陈小杨
分享简介
形式化数学，将数学证明转化为计算机可验证的语言，长期以来一直是少数专家的领域。它要求将每一步推理都精确到机器可验证的程度，没有跳跃，没有“显然”，只有严格的逻辑链条。这种严谨性使得形式化证明在传统上需要耗费大量时间和专业知识，限制了其广泛应用。
Lean语言的形式化表述
随着生成式AI的崛起，这个领域也迎来了新的发展机遇。大语言模型有很强的推理能力，但是在准确性和可靠性方面面临挑战，形式化数学刚好可以弥补这一短板，为AI在数学推理上提供严格的验证框架。反过来，AI也有潜力来帮助自动形式化，完成从自然语言到形式化语言的转换，降低领域门槛，加速证明过程。
在本次分享中，将介绍形式化数学的发展现状，以及和生成式AI交叉的前沿进展。
分享大纲
形式化数学简介
形式化数学与生成式 AI：互补短长
目前的进展
主讲嘉宾简介
徐天一，北京国际数学研究中心研究员。研究方向为自动化定理证明及 Lean 语言元编程。开发了多种用于操作 Lean 语言代码的工具，涵盖数据提取、依赖关系分析和动态交互等功能。同时负责 LeanSearch 的维护。
圆桌嘉宾简介
陈小杨，同济大学特聘研究员。2014年5月获得美国圣母大学数学博士学位，2014-2016年在澳门大学从事博士后研究，并于2016年底入职同济大学。陈小杨的主要研究方向为黎曼几何，在 Geometry and Topology, Advances in Mathematics等期刊发表了多篇研究论文。近期，陈小杨与研究团队开展了大模型在基础数学的应用研究，并计划开发机器学习算法用于发现数学规律，构造数学猜想反例等。
同时陈小杨团队发起了“ ”，旨在训练一个开源数学大模型，将其数学推理能力提升至数学专业博士生水平，同时探索大模型是否具有数学创造能力，以及大模型在前沿数学研究中的潜在能力。邀请数学爱好者和智能探索者共同创建数学大模型。
推荐阅读论文：
Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2023): 21573-21612. https://proceedings.neurips.cc/paper_files/paper/2023/file/4441469427094f8873d0fecb0c4e1cee-Paper-Datasets_and_Benchmarks.pdf
Gao, Guoxiong, et al. "A semantic search engine for Mathlib4." arXiv preprint arXiv:2403.13310 (2024). https://arxiv.org/abs/2403.13310v2
Gao, Guoxiong, et al. "Herald: A natural language annotated Lean 4 dataset." arXiv preprint arXiv:2410.10878 (2024). https://arxiv.org/abs/2410.10878
Lin, Yong, et al. "Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving." arXiv preprint arXiv:2502.07640 (2025). https://arxiv.org/abs/2502.07640
Ying, Huaiyuan, et al. "Lean workbook: A large-scale lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024). https://arxiv.org/abs/2406.03847
Xin, Huajian, et al. "Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data." arXiv preprint arXiv:2405.14333 (2024). https://arxiv.org/abs/2405.14333
直播信息
2025年3月12日 19:00-21:00
报名加入社群（可开发票）
集智斑图链接：https://pattern.swarma.org/study_group/32?from=wechat
扫 码参与 ，加入群聊，获取系列读书会回看权限，共建共享 AI for Math 科学社区，与一线科研工 作者沟通交流，共同推动这一前沿领域的发展。
人工智能与数学读书会启动
数十年来，人工智能的理论发展和技术实践一直与科学探索相伴而生，尤其在以大模型为代表的人工智能技术应用集中爆发的当下，人工智能正在加速物理、化学、生物等基础科学的革新，而这些学科也在反过来启发人工智能技术创新。在此过程中，数学作为兼具理论属性与工具属性的重要基础学科，与人工智能关系甚密，相辅相成。一方面，人工智能在解决数学领域的诸多工程问题、理论问题乃至圣杯难题上屡创纪录。另一方面，数学持续为人工智能构筑理论基石并拓展其未来空间。这两个关键领域的交叉融合，正在揭开下个时代的科学之幕。
为了探索数学与人工智能深度融合的可能性，集智俱乐部联合同济大学特聘研究员陈小杨、清华大学交叉信息学院助理教授袁洋、南洋理工大学副教授夏克林三位老师，共同发起“人工智能与数学”读书会，希望从 AI for Math，Math for AI 两个方面深入探讨人工智能与数学的密切联系。读书会已完结，现在报名可加入社群并解锁回放视频权限。
详情请见：
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
