AIPS: An Olympiad-level AI System for  Algebraic Inequalities

AIPS (Algebraic Inequality Proving System) is a pioneering Olympiad-level AI system for algebraic inequalities. 

By combining symbolic deduction, an efficient search algorithm, and learning methods, AIPS is not only capable of generating large-scale, high-quality inequality theorem dataset, but also effectively solving complex inequality problems. On a test set of 20 International Mathematical Olympiad (IMO) level inequality problems, AIPS successfully solved 10, outperforming state-of-the-art methods. Furthermore, AIPS automatically generated a vast array of non-trivial theorems without human intervention, some of which have been evaluated by professional contestants and deemed to reach the IMO-level. Notably, one theorem was selected as a competition problem in a major city 2024 Mathematical Olympiad. 

Navigation

1. To explore our research, visit the Research section.

2. To view some complex theorems generated by AIPS, visit the Synthetic Olympiad-level Theorems section.

3. To access the synthetic dataset generated by AIPS, visit the Synthetic Training Dataset section.

4. To access the new test set generated by AIPS, visit the Synthetic Testing Set section. 

News

A synthetic test-set has been uploaded!