系列报告

本报告介绍近年来围绕形式化数学与AI for Math基础设施开展的若干研究工作，主要涉及基于定理结构的形式化生成与验证、面向数学文献的项目级形式化生成，以及形式化证明结构的抽象与复用。报告将结合具体研究实践，介绍相关问题的研究背景、技术方法和阶段性进展，并讨论当前工作中面临的问题与后续研究计划。

马万里，复旦大学计算数学博士，现为北京大学北京国际数学研究中心博士后。主要研究方向包括AI for Math、数学自动形式化、数值代数与张量计算。博士阶段围绕张量广义特征值、多重线性系统和在线张量动态模式分解开展理论、算法与应用研究；博士后阶段重点研究数学内容的形式化生成、机器验证与可验证推理，参与面向教材和论文的大规模自动形式化研究，参与设计由抽象数学结构生成具体实例的定理自动形式化方法，主导矩阵分解存在性定理的统一Lean形式化框架，并参与计算数学形式化定理库建设。截至2026年，共发表学术论文7篇，其中第一作者论文4篇，相关成果发表于Journal of Scientific Computing、Journal of Computational and Applied Mathematics及AAAI等期刊和会议。入选北京大学博雅博士后项目，并获中国博士后科学基金面上资助。