【小哈划重点：高小山在数学机械化研究中取得了系统与原创成果，对该领域的发展做出了重要贡献。他提出了几何约束求解的完整高效算法并解决了最佳空间并联机构构型与视觉定位基本问题，将机器证明开拓到自动作图新方向。】
获奖者风采
高小山，中国科学院数学与系统科学研究院研究员、常务副院长，主要从事数学机械化研究，是吴文俊开创、具有重要国际影响的数学机械化领域目前的学术带头人。2019年，荣获第九届吴文俊人工智能杰出贡献奖。
获奖者简介
高小山，现任中国科学院数学与系统科学研究院研究员、常务副院长，主要从事数学机械化研究，是吴文俊开创、具有重要国际影响的数学机械化领域目前的学术带头人。2019年，荣获第九届吴文俊人工智能杰出贡献奖。
建立了微分差分系统机器证明基本方法：微分稀疏结式、微分周形式、差分特征列方法，实质性开拓了数学机械化的适用范围，是数学机械化研究的重要突破。合作建立了几何定理机器证明的消点法，首次实现了定理可读证明的自动生成，极大提高了机器证明的质量，使定理机器证明进入到机器证明可以与传统证明比美的新阶段。针对智能CAD、机器人、计算机视觉等机器智能中的关键问题，发展了几何约束求解的系统高效算法，解决了视觉定位与并联机器人构型基本问题，将数学机械由定理机器证明开拓到自动作图新方向。针对在高端数控智能制造多种重要实用约束，设计了快速的时间最优运动插补控制算法，在国家重大科技专项支持的商用数控系统中实现，显著提高了数控加工精度与速度，在航空制造领域得到应用。
出版专著4部，发表论文130余篇，谷歌学术他引4500余次。曾获国家自然科学二等奖（第三），中科院自然科学一等奖（第二），第36届国际计算机学会SIGSAM/ISSAC杰出论文奖,香港求是杰出青年学者奖，第4届亚洲数学技术会议最佳论文奖，国家十五重大科技成就网络展，吴文俊应用数学奖，国家基金委杰出青年基金。作为首席科学家主持三个数学机械化973项目，获科技部“十一五国家科技计划执行突出贡献奖”。
获奖理由
高小山在数学机械化研究中取得了系统与原创成果，对该领域的发展做出了重要贡献。他提出了几何约束求解的完整高效算法并解决了最佳空间并联机构构型与视觉定位基本问题，将机器证明开拓到自动作图新方向。合作建立了基于不变量的消去理论，使机器证明进入到与传统证明比美的新阶段。将数学机械化核心理论开拓到微分差分系统，开拓了机器证明的适用范围、降低了计算复杂度。针对智能数控加工重要实用约束，设计了快速时间最优插补算法，显著改进了加工效率与精度。
项目介绍
针对智能CAD、机器人、计算机视觉、智能数控加工等机器智能中的重要需求，建立了几何定理机器证明的消点法、微分差分系统机器证明基本方法、发展了几何约束求解的系统高效算法，实质性开拓了数学机械化的适用范围并得到重要应用。具体成果包括：
1. 几何自动作图及其在智能CAD、机器视觉与机器人中的应用
提出了几何自动作图的C树分解法与轨迹相交法，在多项式时间内计算出在等距变换下所有封闭解，将其余问题分解为极小模式，并给出求解多类极小模式的显示公式与快速算法，完整地解决了几何自动作图问题。引进了最一般的空间并联机构GSP平台，发展了代数几何方法求解其运动学正解，对于多种情形首次给出了显示解，解决了具有优良运动学性质的并联机器人构型基本问题。解决了视觉定位基本问题之一P3P解的完全分类公开问题,首次给出P3P问题的完整解析解，给出了数值求解的稳定性判定准则与完整与稳健的求解算法。
2. 几何定理机器证明的消点法
合作建立消点法，将几何不变量引入自动推理，对构造型几何命题发展了完整的消去理论，克服了“中间过程爆炸”难题，首次实现了自动生成可读证明，使几何定理机器证明进入到机器证明可以与传统证明比美的新阶段。消点法已被国外学者在主流自动推理平台Coq、Isabelle/HOL，Theorema中实现并用于安全攸关系统验证、力学系统机器证明等。
3. 微分差分系统的消去理论与高效算法
结式、周形式与特征列方法是数学机械化基本算法,由于存在根本困难，长期未能拓展到微分差分情形。本项目证明了Ritt于1950年提出的微分维数猜想“一般”正确，克服了定义微分周形式的障碍，首次给出微分周形式与微分稀疏结式的严格定义；建立了微分周形式与微分稀疏结式完整理论，引进了微分簇的“微分次数”新不变量，定义了微分簇的周坐标新概念；给出了微分几何机器证明的单指数算法。发现并证明了代数不可约的差分特征列是非平凡的这一关键结果，突破了差分特征列非平凡判定需要无穷次差分的难点，建立了差分特征列算法并用于组合恒等式机器证明。
4. 机器人与高端数控最优插补控制算法
针对在高端数控加工与机器人运动多种重要实用约束，包括jerk、jounce、加工误差、动力学等确定与随机约束，设计了多项式时间的时间最优5轴联动数控机床的运动插补控制算法，在国家重大科技专项“高档数控机床及基础制造装备”支持的商用数控系统中实现，加工效率提高了40%-150%，加工精度显著改进，并应用于航空领域高速高精加工。
实验室简介
中国科学院数学机械化重点实验室是国际计算机数学领域的科研、人才培养、学术交流的主要中心之一。
“数学机械化”是由实验室的创始人吴文俊院士创立的一个研究方向。20世纪70年代，吴文俊提出借助于计算机的强大计算进行自动推理将是信息时代数学发展的重要趋势之一，也将为脑力劳动机械化提供重要支撑。吴文俊建立了几何定理机器证明的“吴方法”与方程求解的 “吴零点分解定理”，成为数学机械化的奠基性成果。吴文俊因此获得国际自动推理最高奖“Herbrand自动推理成就奖”、首届国家最高科技奖、有“东方诺贝尔奖”之称的邵逸夫数学奖，被国家授予首届“人民科学家”荣誉称号。
实验室的中青年科研人员也取得了一系列高水平的科研成果，并获得了十数项国内重要奖励与多项国际奖励，包括国家自然科学二等奖三项，国家技术发明二等奖，ACM/SIGSAM ISSAC杰出论文奖三项等。实验室是我国数学机械化研究的主要组织者。主持国家“973”项目三项，国家基金委优秀创新群体项目等。
数学机械化实验室在几何自动推理、特征列方法、计算微分差分代数几何、智能数控插补等方面在国际上有明显优势。特别是在几何自动推理方面，国际学术界公认实验室做出了开创性成果。数学机械化实验室也是国际符号计算方面的主要中心之一。举例说明，符号计算最权威的国际会议是ACM/SIGSAM ISSAC，已经举办了48届。实验室成员曾经当选为ACM/SIGSAM副主席、ISSAC大会主席（3位）、ISSAC指导委员会主席（3位）、ISSAC程序委员会主席，作ISSAC邀请报告（3次）。国际著名学者M.Singer指出实验室“是国际上符号计算最强的研究群体之一，产生领军人物、有基础意义的研究成果和软件，对整个科学界有很强的影响力”。
获奖感言
十分荣幸获得吴文俊人工智能杰出贡献奖，衷心感谢中国人工智能学会的肯定与鼓励，感谢各位同行的支持。我在吴文俊先生身边工作了30多年，深知他对数学机械化有很高的期望。他希望：“通过数学的机械化，推动脑力劳动机械化”；他展望到：“枪炮使人们在体力上难分强弱，通过脑力劳动机械化，计算机将使人们在智力上难分聪明愚鲁。”我的工作只是吴文俊先生这些宏大设想的一小步。让我们真诚祝愿他的希望尽快成真，祝愿我国人工智能事业蓬勃发展。
（原文标题：《联接数学机械化与人工智能——第九届吴文俊人工智能杰出贡献奖获奖者、中科院数学与系统科学研究院研究员、常务副院长高小山》）
