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. DeepSeek-Prover-V2 shows relative robustness—possibly because it is trained to decompose the problems into sub-problems—but still suffers a 20% performance drop (pass@32). Strikingly, performance remains poor for all models even when formal proofs of the constituent parts are provided in context, revealing that the source of weakness is indeed in compositional reasoning. Our results expose a persisting gap between the generalization behavior of current AI provers and human mathematical intuition.

The Lean 4 environment and the corresponding Mathlib version used in this project follow from DeepSeek-Prover-V1.5. Please first install the correct Lean 4 and Mathlib version following the environment setup guide.

After installing the corresponding Lean 4 environment, please copy the benchmark/ and scripts_eval/ folder to the parent folder where you build your Mathlib. You should get the following file strueture (only show the important folders).

parent_folder/
├── benchmark/
├── configs/
├── mathlib4/
├── prover/
└── scripts_eval/

Please run the following command to test DeepSeek-R1-Distill-Qwen-32B without the thinking block (chat template) under pass@32. This will test the model on the 25 seed problems from Ineq-AMGM.

bash scripts_eval/inference_2gpu.sh -i benchmark/amgm_seed.jsonl -m deepseek-ai/DeepSeek-R1-Distill-Qwen-32B -o results/amgm_seed_r1-distill-qwen-32b_nothink -n 32

The script will: (1) inference using VLLM and extract the Lean code (need 2 gpus); (2) submit the code to REPL and verified by Lean 4 compiler. (no gpu needed)

For DeepSeek-R1-Distill-Qwen-32B with the thinking block, please run

bash scripts_eval/inference_think_2gpu.sh -i benchmark/amgm_seed.jsonl -m deepseek-ai/DeepSeek-R1-Distill-Qwen-32B -o results/amgm_seed_r1-distill-qwen-32b -n 32

To test DeepSeek-Prover-V1.5-RL, Goedel-Prover-SFT, STP, please using the script that test DeepSeek-R1-Distill-Qwen-32B without the thinking block while changing the model to your target model (taking STP as an example).

bash scripts_eval/inference_2gpu.sh -i benchmark/amgm_seed.jsonl -m kfdong/STP_model_Lean -o results/amgm_seed_stp -n 32

For Kimina-Prover-Preview-Distill-7B, please run the following script

bash scripts_eval/inference_kimina_2gpu.sh -i benchmark/amgm_seed.jsonl -m AI-MO/Kimina-Prover-Preview-Distill-7B -o results/amgm_seed_kimina-7b -n 32

For DeepSeek-Prover-V2-7B, please run the following script

bash scripts_eval/inference_dsprover2_2gpu.sh -i benchmark/amgm_seed.jsonl -m deepseek-ai/DeepSeek-Prover-V2-7B -o results/amgm_seed_dsprover2-7b -n 32

The main logic under all these scripts is very similar, and the difference between different scirpts (for DeepSeek-R1-Distill-Qwen-32B, Kimina-Prover-Preview-Distill-7B, and DeepSeek-Prover-V2-7B) is the prompt and the response template.

Note 1: all the scripts can be technically run with 2 H100 80GB GPUs. However, we recommend to use 4 H100 80GB GPUs when testing DeepSeek-R1-Distill-Qwen-32B, Kimina-Prover-Preview-Distill-7B, and DeepSeek-Prover-V2-7B, especially if you want to test with more than 16K generation length, since for some VLLM versions it might cause GPU OOM with only 2 gpus.

Note 2: we highly recommend splitting the job into smaller ones, especially when testing DeepSeek-R1-Distill-Qwen-32B, Kimina-Prover-Preview-Distill-7B, and DeepSeek-Prover-V2-7B or testing models under high budget (pass@3200). We include the SLURM head in each scripts for better parallelization with more GPU resources, please refer to the scripts for more details.

The experiments for DeepSeek-Prover-V1.5-RL+RMaxTX can be reproduced using exactly the same command in the original DeepSeek-Prover-V1.5 repo, by changing the dataset to the benchmark dataset (benchmark/amgm_seed.jsonl) in configs/RMaxTS.py file:

python -m prover.launch --config=configs/RMaxTS.py --log_dir=logs/RMaxTS_results

Please refer to DeepSeek-Prover-V1.5 codebase for more details.

The evaluation code is based on the InternLM Github Repo, and particularly, the evaluation code for MiniF2F, with only minimal modifications. Please follow the repo to install the correct Lean 4 and other corresponding package version, especially LeanDojo.

After installing the corresponding environment, please substitute the MiniF2F by the LeanIneqComp-Dojo , which is the Github Repo of Ineq-Comp tracable by Leandojo and adapted to the Lean 4 version used by InternLM2.5-StepProver.

All the data of our Ineq-Comp benchmark, including the proofs of the seed problems, can be found in the benchmark folder, and is also available on Huggingface.

For Ineq-Simp, which contains Ineq-AMGM, Ineq-Cauchy, and Ineq-MISC, the questions can be found at benchmark/amgm_*.jsonl, benchmark/cauchy_*.jsonl, and benchmark/misc_*.jsonl.

benchmark/comp2_100.jsonl contains 100 inequality problems generated using Ineq-Mix by randomly composing two seed problems from Ineq-Simp.

benchmark/real.jsonl contains 50 real-world inequality problems.

The proof for the 75 seed problems can be found in benchmark/full_answer/ folder. We include the proof for two Lean 4 versions: 4.9, where our main experiments are based on (which is also the version used by DeepSeek-Prover-V1.5), and 4.18, which is the Lean 4 version (stable) used by the interactive Lean 4 web at the time this benchmark is curated.

Our Ineq-Mix framework that can generates more problems (given a pool of base problem) can be found in the composition/ folder.

original_problems.jsonl includes 65 seed problems that can be possibly composed or transformed. The composition rules, the variable-level algebraic transformation rules, and the problem-level algebraic transformation rules are defined in composition/comp_op.py, composition/algebraic_op.py, and composition/algebraic_whole_op.py, respectively. Please refer to composition/mix.py for more details.

If you find our work helps, please consider starring ⭐ us and citing:

@article{zhao2025ineq,
  title={Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities},
  author={Zhao, Haoyu and Geng, Yihan and Tang, Shange and Lin, Yong and Lyu, Bohan and Lin, Hongzhou and Jin, Chi and Arora, Sanjeev},
  journal={arXiv preprint arXiv:2505.12680},
  year={2025}
}