Thinking Machines: Mathematical Reasoning in the Age of LLMs
This work addresses the problem of understanding and improving LLMs' reasoning capabilities in formal mathematics for researchers in AI and machine learning, though it is incremental in nature.
The paper examines the challenges of applying Large Language Models (LLMs) to formal mathematics, highlighting that progress in theorem proving is more difficult than in coding despite similarities, and explores key issues like training trade-offs and the brittleness of proof generation.
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.