2022年11月，ChatGPT的发布如同一颗石子投入湖心，在全球范围内激起了大语言模型的浪潮。一年后的2023年，在复旦校园里，一支名为“数院大神”的学生志愿团队，迎来成立10周年的日子。
十多年来，这支来自复旦数学科学学院的团队，为超过12000名同学提供数学学习支持，累计志愿服务超过16000个小时。2025年，他们又一次获评复旦大学“十佳志愿服务先进集体”。
然而，大模型时代的到来，也给团队带来了新的思考。作为上海数学中心2025级直博生、“数院大神”团队负责人的马行健与成员们不禁自问：如果未来AI能实现全天候、跨学科的即时答疑，“数院大神”将如何持续发挥价值？
为此，团队对各类大模型开展深入测评，结果发现：面对“实变函数学十遍，泛函分析心泛寒”这类让数院学子也犯难的数学专业课，其抽象与艰深也让大模型“幻觉”频生，给出的答案常常出现逻辑跳跃或步骤缺失，看似合理却难以推敲，有时甚至调用超纲知识，让初学者无从跟进，也难以自我评估。
正是看到通用模型局限与团队转型的需要，马行健与队员们决定发挥数学专长，探索AI与教学的深度融合，打造一个真正“懂数学”的智能辅助平台——AI4Math应运而生。
这一设想迅速获得学院公共数学教研室、学工团队及学校人工智能教育教学创新中心的认可与支持，为项目落地铺平道路。
瞄准两大教学痛点
参与AI4Math的“数院大神”成员，都有丰富的答疑或授课经历。
马行健大一加入“大神体验岗”，大二成为正式队员，大三时已担任团队负责人与高等数学习题课老师。这种既是学生、又当“老师”的双重身份，让他能同时理解学习者的困惑，也从授课者视角出发，去设计一套科学的数字方案。
马行健（左）正在答疑
在数学科学学院谢纳庆教授领衔的公共数学教研室的支持下，团队充分吸收学院在高等数学数字化建设中积累的经验与一线教学反馈，最终瞄准了两个核心教学痛点：一是学习诊断闭环缺失，快节奏的标准化课程使得同学们“学完即忘”，师生互动不足也导致难以及时给予学习反馈，让同学们“不知学了什么、不知学的如何、不知为何而学”。
二是大模型数学推理的可信度问题。“简单来说，大模型的输出来自概率化的生成机制，更擅长给出‘看起来最可能’的推导表达，而不是自动确保每一步都满足严格的逻辑约束。”他解释道，“因此在证明题里，一旦出现跳步或漏条件，对初学者可能适得其反。”
基于此，AI4Math项目设定三大目标：让同学们能够看见知识结构、了解学习进展、相信模型推理。
“学生主导开发的产品，其优势在于需求来源于学生长期参与一线教辅工作的经验。” 项目指导教师、计算与智能创新学院副教授、人工智能教育教学创新中心副主任朱东来评价道，“这与教学专家和授课教师的角度有明显不同，同时又结合了数学形式化证明方面的专业知识，具有一定的先进性。”
来自一线教学积累的数据底气
如何实现目标？马行健与团队拥有大模型时代最珍贵的资源——长期积累的教学与答疑实践数据。
“AI4Math项目的数据基础是数院和‘数院大神’团队的长期积累，主要来自进阶数学教材评述体系、真题与习题精讲资源库、结构化笔记与专题讲座资源、进阶学习误区数据库这四个方面”，马行健介绍。
其中，教材评述体系尤为珍贵，由数学科学学院的教授团队亲自参与构建。这一体系系统整合《微积分》《线性代数》等12门经典数学课程的107本教材评述，是同学们打基础的重要依托。
真题与习题精讲资源库的构建，源自“数院大神”团队在指导老师、2025级辅导员丁宇哲推动下持续数年的沉淀与系统梳理。资源库整合了超过500期“每日一题/每周好题”，收录多门数学专业进阶课程近年真题，以及全国大学生数学竞赛专题题库，形成一套覆盖广泛、内容精炼的学习资源体系。
“这些数据是我们在长期工作过程中积累下来的独特财富。”马行健说。与互联网上广泛流通的公开资料不同，这些资源经过“数院大神”团队的反复验证和整理，质量更高，针对性更强。
团队还依托“香蕉空间”建立子空间，积累了结构化的课程笔记与习题解答，并整合了“数海启航”讨论班讲义和复习讲座资料。这些并非简单的课堂记录，而是经过系统梳理、便于复习和查询的知识集合。
此外，团队持续记录学生在进阶课程中的高频疑问，逐步构建起“进阶学习误区数据库”。“这个数据库是持续更新的，我们会在每次授课中不断补充完善。”马行健表示。
自研形式化语言Litex
为了更好地解决现有大模型存在的“幻觉”问题，在朱东来的建议与帮助下，马行健为AI4Math项目组建了一支跨学科团队。
23级数学科学学院博士生、AI Lab实习生沈嘉辰带领小组，负责推进自研形式化语言Litex的开发；22级数学科学学院本科生、“数院大神”团队负责人李昕昊带领小组，负责基于团队原有数据的进一步数据集制作；马行健负责的“形式化语言与大模型微调”讨论班，吸引多位来自数学科学学院、计算与智能创新学院等院系的本科生以及研究生共同参与，通过阅读文献与动手实践，研究如何将形式化语言用于解决“幻觉”问题并增强大模型推理以及教学能力，这种交叉融合也为项目注入了独特优势。
“团队面临的首要课题是如何在现有大模型技术基础上实现自主创新。”马行健坦言。团队选择了“深耕既有研究，寻求差异突破”的策略，希望站在巨人的肩膀上，先把国内外顶尖数学大模型的研究“完完全全深入学习一遍”，再寻找突破点。
对抗大模型在数学推理中的“幻觉”，也是AI4Math必须攻克的核心难题。马行健对此有清醒认识：“目前已有的工作暂时没有完全解决这个问题。”因此，团队正在探索一条不完全相同的技术路径。
朱东来对此表示认同：“对抗大模型‘幻觉’是目前学术界比较有挑战的问题。在数学大模型这个细分领域，目前一种可能的思路是将形式化语言与大模型相结合，实现数学推理的可验证性。”
为此，团队尝试迈出了大胆的一步——自主研发形式化语言Litex，将数学证明过程转化为计算机可验证的代码。
“像Lean4这样的现有形式化语言已经比较成熟，但学习成本高，”马行健介绍，“沈嘉辰学长选择了一个与传统形式化语言不同的新体系，在开发时更兼顾与自然语言的相似度，目标是保持严谨的同时，大幅降低表达和学习难度，把学习门槛缩短到小时级别。”
这门语言目前已在GitHub开源，并登上Hacker News全球趋势榜前十，引发全球开发者围绕形式化语言可用性的讨论。核心开发者沈嘉辰在相关文章中写道：“Litex致力于将形式化证明学习周期从传统的3-6个月缩短至1-2小时，让形式化推理过程变得如同编写数学算式一般自然。”
六大功能支持从智能答疑到个性化学习路径搭建
2025年5月，“数院大神”团队凭借AI4Math项目的初始版本“登堂入释——定制你的数学个性学习管家”荣获复旦大学首届AI应用开发大赛金奖，这次经历不仅验证了技术路线的可行性，更跑通了“从数据到服务”的工作流模式，为后续发展积累了关键经验。
基于扎实的数据基础和技术创新，AI4Math平台在此基础上开发完善了智能答疑、答案评估、定理查询、学术检索、个性推荐和学情分析等六大核心功能。
学生可以上传题目照片获得解答思路，也可以提交自己的解题步骤获得逻辑完整性评估。平台还接入arXiv全球论文库，支持学术检索与前沿论文推荐。
“根据使用学生的过往问答数据，平台能生成个性化的能力评估报告，并推荐适合的题目和教材。”马行健演示道，“我们还提供了知识图谱，清晰展示知识点之间的关联，如推出、包含、前提等关系。”基于这些深度的关联性分析，当检测到学生在某个知识点上存在薄弱环节时，平台能够给出一些学习建议。
团队希望平台不仅能覆盖基础数学课程，还能支持高年级数学专业课。“对于‘实变函数’、‘泛函分析’这些硬课，希望我们独特的结构化笔记和题库能够在未来起到作用。” 马行健说。
一种“师生共创”新范式
项目能够顺利推进，离不开“师生共创”模式的支持。
“我们的项目入选了复旦大学人工智能教育教学创新中心的‘AI+师生共创重点项目’，学校给了我们师资、算力和资金等多方面的支持。”马行健说。
“这种模式打破了以往高校‘教师主导、科研导向’的常规路径，构建起‘师生共创、场景驱动’的新范式。从教师侧来看，从单纯的知识传授者转变为学生学习的设计者、引导者和协同创新者；从学生侧来看，核心在于让学生在解决真实问题的过程中，实现能力结构的整体升级。”朱东来在项目中主要提供三方面支持：明晰应用场景和需求、指导技术路线和框架、协助对接开发和算力资源。
“我不给团队下指令、做决定，而是以提问题、给建议为主。”他分享，当团队提交早期的功能列表和界面设计后，他引导团队思考潜在用户有哪些、他们会通过什么方式使用、希望达到什么目标……这种引导帮助没有系统开发经验的学生团队逐步完善了产品设计。
对马行健来说，参与这个项目带来的成长是全方位的。“一方面，它让我深扎大模型技术前沿，完成了深度的相关知识网络构建；另一方面，它也锻炼了我独立开展研究和团队管理的能力。”
目前，AI4Math平台已在复旦大学校园ehall平台的“智汇岛”和AI3A共创平台上线，并在《高等数学（D）》的班级中进行了初步试用，正在收集师生使用反馈。下一学期将逐步扩展至《高等数学》《线性代数》，再之后将面向数学专业课。
谈及未来，团队有着明确规划：推动数学课程教学向智能化、精准化和规模化升级，并在此基础上推动数学形式化证明与数学大模型的科研突破。
“我们希望这个平台能服务更多同学，真正实现多覆盖、全天候、个性化的智能化教学，从‘被替代’到‘全面升级’。”马行健说。
