数学研究长期面临诸多限制效率的瓶颈问题，而人工智能技术的引入为突破这些瓶颈提供了新的可能。在这样的背景下，“AI for Mathematics”（AI4M）作为一个新兴的交叉研究领域应运而生。本报告将首先从数学研究自身的挑战与需求谈起，阐释为什么数学需要 AI 的深度赋能；继而介绍近年来 AI4M 领域的一些代表性成果，并比较不同技术路线的优势与局限。在此基础上，报告将指出，要显著提升 AI 的数学推理能力，核心在于推进数学知识的形式化，即数学的“数字化”。最后，报告将介绍北京大学 AI4M 团队的整体研究规划，展示团队在形式化模型与工具设计、自动推理系统构建以及高质量评测集开发等方面取得的阶段性成果，并对AI4M 的未来发展进行展望。