| Professor Wen-tsün Wu
is honorary director of the Mathematics Mechanization Research Center
and the Institute of Systems Science at the Chinese Academy of Sciences.
He is well-known in the community of automated reasoning and symbolic
computation for his breakthrough work - Wu's method - on automated
geometric theorem proving. Wu also made important contributions to the
study of the history of Chinese mathematics, for which he was honored
with an invited address at the International Congress of Mathematicians
at Berkeley in 1986. Wu worked for three years in the Bourbaki school
with H. Cartan after he completed his state thesis in Strasbourg
in 1949. His early work and contributions, including the famous Wu
formula and Wu class, have become classical results of topology.
Wu received a number of outstanding awards, held positions and
honorary titles in various academic and governmental organizations,
delivered addresses at many congresses, served as (honorary) editor
for numerous journals, books and book series at both national and
international level. |
 |
Professor
Wu (right) receiving an award
from the Chinese Premier
|
|
| |
There
are essentially two kinds of studies in geometry: geometry
problem-solving and geometry theorem-proving. Typical examples for
the former are geometric constructions, which were well-studied in
ancient Greek mathematics. The creation of analytic geometry in the
17th century with the introduction of coordinates renders it possible
to reduce geometric problems to algebraic ones. With this reduction,
some method of automated deduction involving polynomial manipulations
we have developed may be applied to solve general problems of
constructions as well as various other kinds of problems in geometry.
For geometric constructions, we may talk about the Appolonius Problem
and the Malfatti Problem as examples. Moreover, by introducing coordinates
to turn geometric statements into algebraic assertions, the automated
deduction method may also be applied to the proving of geometric
theorems by means of computers. A lot of difficult theorems
have been so proved or even discovered automatically.
Among these theorems we may mention such celebrated ones bearing the
names of Pascal, Feuerbach, and Morley. Such an automated deduction
method has also been applied, naturally, to geometric problems and
theorems arising from modern technologies. |
|
