大模型时代的到来，给成立10周年的“数院大神”学生志愿团队带来了新思考。上海数学中心2025级直博生、“数院大神”团队负责人的马行健自问：如果未来AI能实现全天候、跨学科的即时答疑，“数院大神”将如何持续发挥价值？
为此，团队对各类大模型开展深入测评，结果发现：面对“实变函数学十遍，泛函分析心泛寒”这类让数院学子也犯难的数学专业课，其抽象与艰深也让大模型“幻觉”频生，给出的答案常常出现逻辑跳跃或步骤缺失，有时甚至调用超纲知识，让初学者无从跟进，也难以自我评估。
看到通用模型局限与团队转型的需要，马行健与队员们决定探索AI与教学的深度融合，打造一个真正“懂数学”的智能辅助平台。AI4Math应运而生。
瞄准两大教学痛点
在学院支持下，团队吸收学院在高等数学数字化建设中积累的经验与一线教学反馈，瞄准了两个核心教学痛点：一是学习诊断闭环缺失，快节奏的标准化课程使得同学们“学完即忘”，师生互动不足也导致难以及时给予学习反馈，让同学们“不知学了什么、不知学的如何、不知为何而学”。二是大模型数学推理的可信度问题。
基于此，AI4Math项目设定三大目标：让同学们能够看见知识结构、了解学习进展、相信模型推理。
“学生主导开发的产品，其优势在于需求来源于学生长期参与一线教辅工作的经验。” 项目指导教师、计算与智能创新学院副教授朱东来评价，“这与教学专家和授课教师的角度有明显不同，同时又结合了数学形式化证明方面的专业知识，具有一定的先进性。”
底气来自一线数据
“AI4Math项目的数据基础是数院和‘数院大神’团队的长期积累，主要来自进阶数学教材评述体系、真题与习题精讲资源库、结构化笔记与专题讲座资源、进阶学习误区数据库这四个方面”，马行健介绍。
其中，教材评述体系尤为珍贵，这一体系系统整合《微积分》《线性代数》等12门经典数学课程的107本教材评述。
真题与习题精讲资源库的构建，整合了超过500期“每日一题/每周好题”，收录多门数学专业进阶课程近年真题，以及全国大学生数学竞赛专题题库，形成一套覆盖广泛、内容精炼的学习资源体系。
团队还依托“香蕉空间”建立子空间，积累了结构化的课程笔记与习题解答，并整合了“数海启航”讨论班讲义和复习讲座资料。这些并非简单的课堂记录，而是经过系统梳理、便于复习和查询的知识集合。
此外，团队持续记录学生在进阶课程中的高频疑问，逐步构建起“进阶学习误区数据库”，“这个数据库是持续更新的，会在每次授课中不断补充完善。”
自研形式化语言
为了更好地解决现有大模型的“幻觉”问题，AI4Math项目组建了一支跨学科团队。
23级数学科学学院博士生、AI Lab实习生沈嘉辰带领小组，负责推进自研形式化语言Litex的开发；22级数学科学学院本科生、“数院大神”团队负责人李昕昊带领小组，负责基于团队原有数据的进一步数据集制作；马行健负责的“形式化语言与大模型微调”讨论班，吸引多位来自数学科学学院、计算与智能创新学院等院系的本科生以及研究生参与，研究如何将形式化语言用于解决“幻觉”问题并增强大模型推理以及教学能力。这种交叉融合为项目注入了独特优势。
团队尝试迈出了大胆的一步——自主研发形式化语言Litex，将数学证明过程转化为计算机可验证的代码。
这门语言目前已在GitHub开源，并登上Hacker News全球趋势榜前十，引发全球开发者围绕形式化语言可用性的讨论。核心开发者沈嘉辰在相关文章中写道：“Litex致力于将形式化证明学习周期从传统的3-6个月缩短至1-2小时，让形式化推理过程变得如同编写数学算式一般自然。”
六大功能支持
2025年5月，“数院大神”团队凭借AI4Math项目的初始版本“登堂入释——定制你的数学个性学习管家”荣获学校首届AI应用开发大赛金奖。
基于扎实的数据基础和技术创新，AI4Math平台在此基础上开发完善了智能答疑、答案评估、定理查询、学术检索、个性推荐和学情分析等六大核心功能。
学生可以上传题目照片获得解答思路，也可以提交自己的解题步骤获得逻辑完整性评估。平台还接入arXiv全球论文库，支持学术检索与前沿论文推荐。
目前，AI4Math平台已在校园ehall平台的“智汇岛”和AI3A共创平台上线，并在《高等数学（D）》的班级中进行了初步试用，正在收集师生使用反馈。将逐步扩展至《高等数学》《线性代数》，再之后将面向数学专业课。
本报记者 赵天润
