"数学机械化"是我国数学家吴文俊先生在七十年代末开始倡导的一个研究领域，是脑力劳动机械化在数学科学的学术实践。数学机械化思想继承了中国古代数学的传统，它的着眼点在数学，但又具有明显的交叉性。

　　所谓机械化是指刻板化与规格化。十七世纪以来，以蒸气机为代表的工业革命是以机器代替人的体力劳动，数学机械化则是用计算机部分代替人类的脑力劳动。今天电子计算机的飞速发展使得数学的机械化正在逐步成为现实。在数学发展过程中，可以看到演绎倾向与算法倾向的此消彼长。两种倾向总是交替地处于主导地位。值得注意的是，探询新算法可以导致数学的重大发现，如解析几何与微积分；而且构造性数学往往具有很高的实用价值。数学机械化研究的深入开展，不仅会进一步丰富数学科学的传统内容，也将进一步丰富其交叉性学科的内容，从而在总体上促进数学科学的发展。

　　数学机械化不仅是数学研究的实质性进展，也为很多高科技问题的解决提供了有力的工具。我们的方法已在许多高科技领域获得了一批理论成果，具备了解决尖端技术产业中实际问题的条件。包括曲面造型，机器人位置分析，几何设计，计算机视觉，智能ＣＡＤ，信息安全和数字图象的高速高保真传输。通过进一步努力，这些理论研究成果有望能够实实在在地解决若干项技术问题为促进我国技术产业的发展做出积极的贡献。

　　数学机械化研究又有明显的交叉性。除高科技领域外，数学机械化的方法还被成功地用于解决其他领域的很多问题：理论物理中的杨振宁－Baxter方程求解， 天体力学中共心多体问题， 化学平衡中的方程求解，小波构造的优化， 命题逻辑与一阶谓词逻辑中的定理证明，非线性发展方程的行波解的算法等等。

　　在国际上，计算机与数学的交叉正在成为数学研究新的增长点,出现了计算代数、计算群论、计算几何、计算数论等新兴学科。符号计算是研究在计算机上进行准确的数学演算和与之相关的数学理论的学科，是数学机械化的主要工具。近年来一批专业化的学术机构已在世界各地纷纷成立。符号计算软件Maple, Mathematica已经在数学与工程领域被广泛使用。８０年代以来，解（微分）代数多项式方程组是国际符号计算界的热点，其主要方法是Groebner基方法。90年代欧共体跨国研究项目 POSSO(POlynomial System SOlving) 及作为POSSO的延续项目FRISCO关注的问题，与我们开展数学机械化研究课题有许多相同之处。所不同的是，我们所用的是我国数学家自己发展起来的一套方法和理论。

　　自动推理是与数学机械化密切相关的学科。自动推理源于人工智能，主要研究推理的自动化与机械化。国外主要以逻辑为基础开展自动推理研究，而吴方法的基础是代数几何。国际上自动推理界在注意发展新方法的同时，积极开展应用研究，如程序正确性验证,自动程序生成等。

　　1990年，中国科学院在批准成立数学机械化中心。数学机械化中心建立十年以来，取得了一系列高水平的科研成果，并获得了十项国内重要奖励与两项国际奖励。特别值得指出的两项奖励是（1）吴文俊先生获1997年自动推理最高奖"Herbrand自动推理杰出成就奖"。这一荣誉进一步表明吴方法已经被国际学术界认为是自动推理领域最基本与经典性工作。（2）由于在数学机械化与拓扑学方面的杰出贡献，吴文俊先生于2000年获得首届"国家最高科学技术奖"。

　　数学机械化研究得到国家领导部门的充分肯定和大力支持。国家科技部在"21世纪科学发展趋势"的报告中将数学机械化列为重大科学问题，国家自然科学基金委员会和中国科学院在"九五"规划中，都将数学机械化列为优先发展的研究领域。

　　数学机械化中心作为主要承担单位，主持了八五国家攀登计划项目"机器证明及其应用"，九五攀登项目"数学机械化及其应用"，"973"项目"数学机械化与自动推理平台"，"数学机械化方法及其在信息技术中的应用"以及"数学机械化方法及其在数字化设计制造中的应用"并以这些项目为依托积极组织国内外数学机械化合作研究与学术交流。经过十多年的努力, 数学机械化中心已经成为国际数学机械化研究、学术交流与人才培养的中心。

　　2003年, 数学机械化中心与信息安全中心联合成立了数学机械化重点实验室。

　　当前信息技术正在给社会生产力带来一场革命，但由于大量敏感信息通过互联网进行交换，信息的不安全性带来严重的社会问题。信息安全理论是研究信息在传输或存储过程中保证信息的"可靠性"、"完整性"、"秘密性"、"真实性"等要求的一门科学，它以数学和计算机科学等学科为基础，现代密码学和纠错编码理论等都是信息安全理论的基础。

　　密码学自1976年Differ和Hellman提出公钥密码体制以来得到了迅猛发展。1985年Koblitz和Miller提出将椭圆曲线用于公钥密码体制，他们第一次用椭圆曲线成功地实现了已有的一些公钥密码算法包括Differ-Hellman算法。现在椭圆曲线密码体制不仅是一个重要的理论研究领域，而且已经作为民用信息安全技术走向产业化。

　　近二十年来，数学和计算机科学中的一些强有力工具和最新研究成果被用到编码理论和密码学中，不仅促进了编码理论和现代密码学的飞速发展，也刺激了数学和计算机科学中的一些分支的发展。

　　(1)利用代数组合、代数数论、计算代数和有限几何的经典工具和最新成果来研究信息科学，特别是编码理论，在当前是数学家和通信技术专家的公同的领域，也是信息科学中的一个热门的研究方向。 (2) 代数几何码是上世纪八十年代由苏联数学家发现的，这一发现使数学中最抽象的分支之一――代数几何，通过编码理论被天才地用到通信工程中去。 由于代数几何码的卓越的纠错和检错性能，持续二十多年，代数几何码的研究仍然是信息论中的一个热点。 (3)Turbo码是法国学者1993年发现的一种新的差错控制码，这种码的纠错性能几乎接近Shannon限，在诸如远程数据通信、数据的磁记录等广泛的应用领域是性能最好的码。 (4) 时空码（即Space-Time码）是美国学者Tarokh 和 Calderbank 等人几年前发现的一种码，它用在多通道、多天线、无线通信信道--例如手机通信中，可以极大地改进这些信道的性能。 (5) 计算的复杂性理论和Shannon的信息论是现代密码学的两大理论支柱。复杂性理论作为数学和信息科学共同的领域，将受到更加广泛的关注。 (6) 量子纠错码和量子密码是量子信息论的两个基本方面，它们都基于量子计算和量子算法。研究量子计算和量子算法是当今信息科学中的最前沿方向之一。

　　数学机械化重点实验室研究方向

　　本实验室以基础研究为主，同时兼顾应用研究，采取基础研究带动应用研究的思路。研究方向可以分为： 理论与方法研究,应用研究与智能软件开发。具体讲 （1）理论与方法研究：构造性代数几何，构造性微分代数几何，构造性实代数几何，计算机代数，编码密码理论，离散几何，量子计算与方法，代数方程求解的混合算法，自动推理； （2）应用基础研究：信息安全，在理论物理、力学中的应用，在机器人中的应用，几何自动作图与智能CAD，计算机视觉中的应用，信息安全与密码中的应用； （3）基于吴方法的智能软件平台的开发。

The Key Laboratory of Mathematics-Mechanization (KLMM) is a research group within the Academy of Mathematics and System Sciences (AMSS) in the Chinese Academy of Sciences (CAS),  Beijing, China. 

The founder is Professor Wen-tsun Wu.

The current director is Professor Lihong Zhi

The primary goal of the Key Laboratory of Mathematics-Mechanization  is to integrate and develop theories, algorithms and softwares for automated reasoning, cryptographic and coding theory, differential and difference equationsin mathematics physics, geometric constraint-solving, polynomial equation-solving,
symbolic computation and hybrid symbolic-numeric computation.

Main research interests of our lab include:

1.   Automated theorem-proving in elementary and differential geometry

2.   Computational differential and difference algebra

3.   Clifford algebra and geometric algebra

4.   Computer-aided geometric design

5.   Symbolic integration and summation, Wilf-Zeilberger  theory

6.   Solving polynomial equations by exact methods (e.g. the the Ritt-Wu method, Groebner bases, resultants, etc)

7.   Solving polynomial equations by hybrid symbolic-numeric methods (e.g. structured matrices, approximate factorization)

8.   Theoretical and algorithmic research in cryptographic and coding theory

9.   Symbolic methods in nonlinear differential equations

10.  Mathematical chemistry and biology.