Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving of Inequalities
Haoyu Zhao, Yihan Geng, Shange Tang, Yong Lin, Bohan Lyu, Hongzhou Lin, Chi Jin, Sanjeev Arora
LLM-based formal proof assistants (e.g., in Lean) hold great promise for automating mathematical discovery. But beyond syntactic correctness, do these systems truly understand mathematical structure as humans do? We investigate this question through the lens of mathematical inequalities---a fundamental tool across many domains. While modern provers can solve basic inequalities, we probe their ability to handle \emph{human-intuitive compositionality}. We introduce Ineq-Comp, a benchmark built from elementary inequalities through systematic transformations, including variable duplication, algebraic rewriting, and multi-step composition. Although these problems remain easy for humans, we find that most provers---including Goedel, STP, and Kimina-7B---struggle significantly, with only DeepSeek-Prover-V2 showing relative robustness. Despite being designed to decompose the problems into sub-problems and should easily handle the \emph{human-intuitive compositionality}, DeepSeek-Prover-V2 also suffers a 20\% performance drop on these transformations under pass@32. Strikingly, performance remains poor even when provers are given formal proofs of the constituent parts, revealing a core weakness in compositional reasoning. Our results expose a persistent gap between human mathematical intuition and the generalization abilities of current AI provers---especially in their handling of compositional structure in formal reasoning.