从解题到科研：LLM 驱动的形式化数学如何走向研究前沿
From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier
一篇综述系统梳理了 LLM 驱动的形式化数学如何从孤立定理证明扩展到选题、定义与猜想构建、结果关联等研究活动，并将证明生成方法归为训练策略、推理时搜索与适配、智能体工作流三类。文章强调形式证明通过检查并不等于捕捉到原问题或构成新数学贡献，据此区分定理基准、代码库任务、形式化项目与研究主张四类证据。作者提出数据与评估、数学关系表示、猜想与概念生成、可靠工具集成、人机协作五项优先方向。
Authors:Eric Jiang, Xiao Liang, Junyi Zhang, Justin Baker, Zhi Zhang, Yingjia Wan, Yubei Li, Jinxi Yu, Mengting Li, Haikang Deng, Alexander Taylor, Rushil Raghavan, Michael Simon, Hyunsik Chae, Jia-Chen Gu, Xinjie He, Kyle Hess, Ethan Ji, Yiwen Kou, Tzu-Han Lin, Jiachen Lu, Jack Mauro, Vigyan Sahai, Zheng Tan, Hengli Li, Yikai Zhang, Kyle Zheng, Lunji Zhu, Dong Liu, Jasdeep Sidhu, Isaac Hair, Eniuce Jun, Ying Nian Wu, Andrea L. Bertozzi, Kai-Wei Chang, Raghu Meka, Matthew Sottile, Nanyun Peng, Amit Sahai, Terence Tao, Wei Wang
Abstract:Large language models have made rapid progress in generating machine-checked proofs for well-defined mathematical problems. Extending this progress to research mathematics requires more than solving isolated theorems. Research involves choosing questions, developing definitions and conjectures, connecting results, and combining formal proofs with expert judgment. This survey examines how LLM-driven systems can support these broader activities. We review formal-mathematics tasks, datasets, and autoformalization, and organize proof-generation methods into three overlapping areas: training strategies, inference-time search and adaptation, and agentic workflows. We then examine benchmark results, selected research projects, and platforms for collaborative mathematical work. A central distinction runs throughout the survey: checking a formal proof does not by itself establish that it captures the intended problem or makes a new mathematical contribution. We therefore distinguish theorem benchmarks, repository tasks, formalization projects, and research claims, and discuss the evidence needed to assess each. Finally, we identify five priorities for progress: better data and evaluation, representations of mathematical relationships, conjecture and concept generation, reliable tool integration, and human--AI collaboration. Together, these perspectives connect advances in proof generation to the practical demands of mathematical research.
| Subjects: | Computation and Language (cs.CL); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2607.07779 [cs.CL] |
| (or arXiv:2607.07779v4 [cs.CL] for this version) | |
| https://doi.org/10.48550/arXiv.2607.07779 arXiv-issued DOI via DataCite |
Submission history
From: Eric Jiang [view email]
[v1]
Wed, 8 Jul 2026 17:46:36 UTC (1,544 KB)
[v2]
Mon, 19 Oct 2026 16:53:53 UTC (2,981 KB)
[v3]
Mon, 2 Nov 2026 19:18:01 UTC (7,892 KB)
[v4]
Wed, 4 Nov 2026 11:31:48 UTC (7,902 KB)
来源：arXiv cs.CL · arxiv.org