Abstract. There are many computer software packages for solving or proving difficult mathematical problems or theorems in automatic mode, but most of them are implemented as a black-box manipulation, and sometimes depend upon too deep mathematics. So, they would not meet the requirement of education. It will be illustrated in this talk how to make use of symbolic computation to deal with some interesting and hard problems, say, polynomial inequality proving, with a little mathematics in a "readable" mode or a computer-aided mode, which can better be understood and accepted by more readers. A program named SDS is designed for polynomial inequality proving, or in other words, for decision of non-negativity of polynomials. The basic idea is: split the variables into smaller nonnegative quantities, then, collect the terms and see whether the coefficients are all nonnegative. The method has been used to prove symmetric polynomial inequalities for so many years that the origin is unavailable. This is a heuristic, not a complete algorithm. However, it has been demonstrated to be very efficient in practice. Quite a number of polynomial inequalities could not be proven until program SDS is employed.