| |







| |

Mathematics-Mechanization tries to deal with mathematics in a constructive and algorithmic manner so that the reasonings become mechanical, automated, and as much
as possible intelligence-lacking, with the results of lessening the painstaking
heavy brain-labor.
In late seventies, Wen-tsun Wu invented a method for proving theorems in geometry
automatically, which was considered as a breakthrough of the field of automated
reasoning, and is called Wu's method in the literature. This method can also be
applied to solving polynomial equations and proving theorems in differential geometry.
Wu and his students formed the Mathematics-Mechanization Research Group at the
Institute of Systems Science around 1985. Based on the conviction that mathematics
-mechanization opened some of the most promising directions on the boundary
between mathematics and computer science, and had great potential applications in
physics and information sciences, the Chinese Academy of Sciences established the
Mathematics-Mechanization Research Center (MMRC) at the Institute of Systems
Science in 1990. Research work completed at MMRC and further recognition of
mathematics-mechanization led to the establishment of the Key Laboratory of
Mathematics Mechanization (KLMM) within the Academy of Mathematics and
System Sciences in the Chinese Academy of Sciences (CAS) in 2002. Current
research
directions of the laboratory include not only mathematics-mechanization, but
also cryptography and mathematical physics .
|
|
|