Reproduce “Proving Olympiad Algebraic Inequalities without Human Demonstrations” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Chenrui Wei, Mengzhou Sun, Wei Wang
AIPS combines a hand-built symbolic inequality engine with a curriculum-trained neural value model to generate and prove ternary and quaternary Olympiad-style inequalities without complete human proof demonstrations. It generated 191,643 synthetic theorems and solved 10 of 20 problems in the MO-INT-20 benchmark, outperforming the evaluated language-model, heuristic-search, and proof-assistant baselines.
Key insights
- Learning is used primarily to control symbolic search rather than to replace formal deduction: every accepted proof step is checked by the symbolic engine.
- Curriculum training improves the search heuristic, raising performance on the benchmark from 7 solved problems with the pretrained model or depth heuristic to 10 solved problems.
- Readable Olympiad-style proofs can emerge from combining standard inequalities with algebraic transformations, although the system remains dependent on its manually designed theorem and operation library.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.