Solving Inequality Proofs with Large Language Models
Authors: name: Jiayi Sheng, name: Luna Lyu, name: Jikai Jin, name: Tony Xia, name: Alex Gu, name: James Zou, name: Pan Lu
Organization: Stanford AI

Inequality proving, crucial across diverse scientific and mathematical
fields, tests advanced reasoning skills such as discovering tight bounds and
strategic theorem application. This makes it a distinct, demanding frontier for
large language models (LLMs), offering insights beyond general mathematical
problem-solving. Progress in this area is hampered by existing datasets that
are often scarce, synthetic, or rigidly formal. We address this by proposing an
informal yet verifiable task formulation, recasting inequality proving into two
automatically checkable subtasks: bound estimation and relation prediction.
Building on this, we release IneqMath, an expert-curated dataset of
Olympiad-level inequalities, including a test set and training corpus enriched
with step-wise solutions and theorem annotations. We also develop a novel
LLM-as-judge evaluation framework, combining a final-answer judge with four
step-wise judges designed to detect common reasoning flaws. A systematic
evaluation of 29 leading LLMs on IneqMath reveals a surprising reality: even
top models like o1 achieve less than 10% overall accuracy under step-wise
scrutiny; this is a drop of up to 65.5% from their accuracy considering only
final answer equivalence. This discrepancy exposes fragile deductive chains and
a critical gap for current LLMs between merely finding an answer and
constructing a rigorous proof. Scaling model size and increasing test-time
computation yield limited gains in overall proof correctness. Instead, our
findings highlight promising research directions such as theorem-guided
reasoning and self-refinement. Code and data are available at
https://ineqmath.github.io/.