Investigate AIPS: An Olympiad-level AI System for Algebraic Inequalities

[deanwampler]

From the AIPS website:

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.

In our context, what's interesting here is the rigor of this project. Can we learn lessons of use for our project?