当AI遇上数学：大语言模型如何掀起一场形式化数学的革命？ | Deep Talk

随着大语言模型在内容创作、代码生成与科学问答等领域掀起巨大变革浪潮，以严谨逻辑与精密结构著称的数学领域也迎来了深刻的转型契机。 当前，数学理论的复杂性不断提升，许多重要定理的证明规模已远超传统人工审阅的能力边界。动辄数百页的证明不仅挑战了同行评审的极限，更暴露出人工验证 过程的缓慢与脆弱性。针对这一困境，形式化数学方法开始成为重要的解决路径。这一方法通过将数学命题严格表达为形式逻辑语言，并借助计算机进行自动化验 证，有效地提升了定理证明的准确性和可靠性。 在形式化数学日益成为趋势的背景下，来自爱丁堡大学的博士研究生辛华剑自2022年起致力于将大语言模型技术与形式化数学方法结合，曾分别在DeepSeek和字节 跳动Seed团队进行相关研究。 2025年5月9日，辛华剑在由剑桥中国AI协会、锦秋基金、清华大学学生通用人工智能协会、 清华大学学生创业协会联合举办的主题分享会上，以《大语言模型时代 的形式化数学革命》为题，详细阐述了形式化数学的历史演进、现状挑战以及未来发展方向。 他认为： 以下内容为此次报告的整理与深化，经由分享人本人审阅补充。 引言 当大语言模型（LLM）以空前规模席卷内容创作与科学研究等领域之际 ...