中国科学院系统科学研究所的数学机械化重点实验室

“数学机械化”是中国数学家吴文俊先生在七十年代末开始倡导的一个研究领域，是脑力劳动机械化在数学科学的学术实践。数学机械化思想继承了中国古代数学的传统，它的着眼点在数学，但又具有明显的交叉性。所谓机械化是指刻板化与规格化。十七世纪以来，以蒸气机为代表的工业革命是以机器代替人的体力劳动，数学机械化则是用计算机部分代替人类的脑力劳动。今天电子计算机的飞速发展使得数学的机械化正在逐步成为现实。在数学发展过程中，可以看到演绎倾向与算法倾向的此消彼长。两种倾向总是交替地处于主导地位。值得注意的是，探询新算法可以导致数学的重大发现，如解析几何与微积分；而且构造性数学往往具有很高的实用价值。数学机械化研究的深入开展，不仅会进一步丰富数学科学的传统内容，也将进一步丰富其交叉性学科的内容，从而在总体上促进数学科学的发展。数学机械化不仅是数学研究的实质性进展，也为很多高科技问题的解决提供了有力的工具。实验室的方法已在许多高科技领域获得了一批理论成果，具备了解决尖端技术产业中实际问题的条件。包括曲面造型，机器人位置分析，几何设计，计算机视觉，智能CAD，信息安全和数字图象的高速高保真传输。通过进一步努力，这些理论研究成果有望能够实实在在地解决若干项技术问题为促进中国技术产业的发展做出积极的贡献。数学机械化研究又有明显的交叉性。除高科技领域外，数学机械化的方法还被成功地用于解决其他领域的很多问题：理论物理中的杨振宁－Baxter方程求解，天体力学中共心多体问题，化学平衡中的方程求解，小波构造的优化，命题逻辑与一阶谓词逻辑中的定理证明，非线性发展方程的行波解的算法等等。在国际上计算机与数学的交叉正在成为数学研究新的增长点,出现了计算代数、计算群论、计算几何、计算数论等新兴学科。符号计算是研究在计算机上进行准确的数学演算和与之相关的数学理论的学科，是数学机械化的主要工具。近年来一批专业化的学术机构已在世界各地纷纷成立。符号计算软件Maple，Mathematica已经在数学与工程领域被广泛使用。80年代以来，解（微分）代数多项式方程组是国际符号计算界的热点，其主要方法是Groebner基方法。90年代欧共体跨国研究项目POSSO(POlynomialSystemSOlving)及作为POSSO的延续项目FRISCO关注的问题，与我们开展数学机械化研究课题有许多相同之处。所不同的是我们所用的是我国数学家自己发展起来的一套方法和理论。自动推理是与数学机械化密切相关的学科。自动推理源于人工智能，主要研究推理的自动化与机械化。国外主要以逻辑为基础开展自动推理研究，而吴方法的基础是代数几何。国际上自动推理界在注意发展新方法的同时积极开展应用研究，如程序正确性验证,自动程序生成等。