Benchmarks on Vasile Problems 20250724

[ForeverHaibara]

Date: 20250724
Last commit: 01a8b2d

Benchmark Description

Problems are collected from Mathematical Inequalities (Vasile Cirtoaje) Volume 1, Volume 2 Chapter 1, and Volume 3, evaluated on July 24, 2025. Test data can be found in triples/benchmarks/problems/books/vasile.py. Problems are indexed by "{volume number}{chapter number}{index}", e.g., "p31169" means Volume 3, Chapter 1, Problem Number 169. N-variate or transcendental problems are excluded from the test data. Among 775 test problems:

• 586 (75.61%) are solved
• 144 (18.58%) failed
• 45 (5.81%) are skipped as they are not expected to be solved within time or memory budget

Note:

• There are chances of typos in the problem inputs, which will get some problems wrongly tested.
• There are chances of "singular" solutions, which use zero denominators.

Sorted test problems downloadable from Testing Vasile Problems 20250724.pdf

Scatter plot of solving time (by second) and solution length (by char):

Comments

The current code merely uses changes of variables. Some problems can be solved easily via sum-of-squares after a suitable transformation. For example: Volume 3, Chapter 2, Problem 93, p6: Given $a - b \geq 0$, $b - c \geq 0$, $c - d \geq 0$, $d \geq 0$, prove that: $a + b + c + d - 4 \sqrt[4]{a b c d} - \frac{4 \left(\sqrt{b} - \sqrt{d}\right)^{2}}{3}\geq 0.$ This would be enhanced in the future.

Future work: More benchmarks? Comparison with LLM provers?