标题： 思考机器：大语言模型时代中的数学推理 显示英文标题

标题： Thinking Machines: Mathematical Reasoning in the Age of LLMs

摘要： 大型语言模型（LLMs）在结构化推理和符号任务方面表现出色，其中编程成为其特别强的一项能力。 这种成功引发了越来越多的兴趣，将LLMs应用于数学领域，包括非正式的问题解决和形式化的定理证明。 然而，尽管编程和证明构造之间存在表面相似性，形式数学方面的进展却证明要困难得多。 这种差异引发了一些关于LLMs如何“推理”、它们如何被监督以及它们是否内部跟踪计算或演绎状态的概念的重要问题。 在本文中，我们关注该领域的最新进展，重点介绍最近的模型和基准，并探讨机器学习与数学认知交叉处的三个核心问题：（i）形式数学与非形式数学作为训练领域之间的权衡；（ii）为什么证明生成仍然比代码合成更脆弱的更深层次原因；（iii）以及LLMs是否代表了动态逻辑状态的概念，或者仅仅是模仿这一概念。 我们的目标不是划定硬性边界，而是确定当前的局限在哪里，以及它们可能如何被扩展。 显示英文摘要

摘要： Large Language Models (LLMs) have shown remarkable abilities in structured reasoning and symbolic tasks, with coding emerging as a particular area of strength. This success has sparked growing interest in applying LLMs to mathematics, both in informal problem-solving and formal theorem proving. However, progress in formal mathematics has proven to be significantly more difficult, despite surface-level similarities between programming and proof construction. This discrepancy raises important questions about how LLMs ``reason'', how they are supervised, and whether they internally track a notion of computational or deductive state. In this article, we address the state-of-the-art of the discipline, focusing on recent models and benchmarks, and explore three central issues at the intersection of machine learning and mathematical cognition: (i) the trade-offs between formal and informal mathematics as training domains; (ii) the deeper reasons why proof generation remains more brittle than code synthesis; (iii) and the question of whether LLMs represent, or merely mimic, a notion of evolving logical state. Our goal is not to draw hard boundaries, but to identify where the current limits lie, and how they might be extended.