CADE-14 Invited Speakers

Observing the equivalence between analytic geometry and plane geometry, Professor Wu demonstrated how geometric problems can be transformed into algebraic problems, so that algebraic methods can then be used to solve, automatically, geometric problems. Professor Wu illustrated the effectiveness of his approach by providing automatic proofs in a dazzling array of problem domains, including plane geometry, algebraic differential geometry, non-Euclidean geometry, affine geometry, and non-linear geometry. Not limiting applications to geometry alone, Professor Wu also gave mechanical proofs of Newton's Gravitational Laws from Kepler's Laws and of problems in chemical equilibrium problems and robotics. Professor Wu's work turned geometry theorem proving into one of the most successful research enterprises in automated theorem proving. Indeed, there are few areas for which one can claim that machines proofs are superior than human, and geometry theorem proving is one of them.

In addition to geometric theorem proving, Professor Wu has also made important contributions in topology and the history of Chinese mathematics.