KLMM


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 .