本书系统总结了作者及其合作者近十年来在不等式数学机械化领域的一系列研究成果及其软件(SCHUR01)实现。SCHUR01是基于作者提出的“分拆—降维—降幂—综合”等算法原理开发的具有自动发现功能的新颖的不等式证明软件，适用于一般代数式乃至任意维数任意次数的多项式的半正定判定及最优化问题。