Thinking Machines: Mathematical Reasoning in the Age of LLMs

TL;DR

This paper reviews the capabilities and limitations of large language models in mathematical reasoning, highlighting challenges in formalized mathematics and exploring the nature of reasoning and state representation in these models.

Contribution

It provides a comprehensive analysis of recent models and benchmarks, discussing the differences between code and proof generation, and questions the internal reasoning processes of LLMs.

Findings

Proof synthesis is more brittle than code generation.

LLMs may emulate rather than genuinely represent logical states.

Trade-offs exist between traditional and formalized mathematics in training.

Abstract

Large Language Models (LLMs) have demonstrated impressive capabilities in structured reasoning and symbolic tasks, with coding emerging as a particularly successful application. This progress has naturally motivated efforts to extend these models to mathematics, both in its traditional form, expressed through natural-style mathematical language, and in its formalized counterpart, expressed in a symbolic syntax suitable for automatic verification. Yet, despite apparent parallels between programming and proof construction, advances in formalized mathematics have proven significantly more challenging. This gap raises fundamental questions about the nature of reasoning in current LLM architectures, the role of supervision and feedback, and the extent to which such models maintain an internal notion of computational or deductive state. In this article, we review the current state-of-the-art in mathematical reasoning with LLMs, focusing on recent models and benchmarks. We explore three central issues at the intersection of machine learning and mathematical cognition: (i) the trade-offs between traditional and formalized mathematics as training and evaluation domains; (ii) the structural and methodological reasons why proof synthesis remains more brittle than code generation; and (iii) whether LLMs genuinely represent or merely emulate a notion of evolving logical state. Our goal is not to draw rigid distinctions but to clarify the present boundaries of these systems and outline promising directions for their extension.