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

机器之心报道 编辑：大盘鸡、泽南 DeepSeek R2 的前奏？ 五一劳动节到了，DeepSeek 的新消息可没停下来。 前些天到处都在流传着 DeepSeek-R2 即将发布的传言，DeepSeek 确实有新动作，不过大家没等来 R2，等来的是 DeepSeek-Prover-V2，它当然也是 开源的。 Prover-V2 在定理证明赛道上实现了业内最佳性能，在 MiniF2F 测试中达到了 88.9% 的通过率，在 AIME 24、25 上也有不错的分数。 在 4 月 30 日晚，机器学习协作平台 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技术细节。 | Models | | --- | 其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5- Base 构建，并支持最长 32K tokens 的上下文长度扩展。 要一句话总结 DeepSeek-Prover-V2 到底是什么？ 它是一款专为「数学 AI 编程语言」L ...