近日，在首届全国大学生“启真问智”人工智能模型&智能体大赛决赛中，由我校数学系副教授张振指导的2023级数学与应用数学专业本科生孙艺峰、符逸铭团队斩获一等奖。

符逸铭代表领奖（左四）

        大赛聚焦 “AI for Education”主题，参赛作品覆盖了教育场景的多个痛点。面对形式化数学（Lean4）证明晦涩难懂与大模型（LLM）翻译频出偏差的现实场景，比赛团队运用创造性的Agent框架，设计出“Lean-Sketch：定理依赖关系增强的Lean解释Agent”。该方案以Lean4元编程与Python脚本为基础，首先结合Jixia工具跨文件提取Lean证明依赖，并通过图算法构建起Common Knowledge Base；随后，利用LLM选择器从该知识库中筛选出证明所需的核心引理与定义；最后，通过few-shot prompts引导并与编译器交互的LLM翻译器，强化对定理的理解，进而生成贴近人类教科书数学语言的自然语言证明。该方案构造了跨文件的pipeline，实现了可控层数的跨文档依赖解析，可处理Mathlib中从初等数论到代数几何的任意定理。该作品能忠实地把形式化语言转换成自然语言，其提出的Agent框架不仅为此类翻译难题（形式化语言到自然语言）提供了新思路，更为AI4Math领域的发展贡献了一个兼具实用价值与前瞻性的工程范本。

        本次大赛由浙江大学主办，阿里云提供支持，为全国高校优秀本科生搭建起探索AI创造与交流平台。自2025年5月启动以来，共吸引全国41所高校的120余份作品报名参赛，经过多轮筛选，40支团队晋级决赛。