报告题目：不等式自动证明的区间分析方法----以球面五点问题为例

报告人：电子科技大学侯晓荣教授

报告时间：2024年6月27日10:00--11:00

报告地点：立志楼A422

摘要：在数学的各个分支领域， 人们希望用相对简单而易于控制的对象去把握复杂的事物，于是产生了不等式。 不等式在数学研究中发挥着显著的作用。在吴先生的倡导并身体力行下，数学机械化领域蔚然已成大气。吴先生对不等式类问题的算法化和机械化问题多有研究, 并多次在数学机械化的各类会议中提及不等式自动证明的困难性。以往相关的工作，集中于处理半代数集问题，其效率主要体现在低维以及约束条件较简单的问题上。面对如“球面5点”之类问题，尽管该问题实质仍是半代数集问题，但变量个数较多、约束关系较复杂，这些方法仍一时难以处理。
         球面5点问题可以追溯到1931年, 是一个长期悬而未决的难题。 有大量的文献研究此类问题 , Smale把这类问题列为21世纪的数学问题之一。针对此类不等式的自动证明，我们提出了区间分析的方法， 用这个方法证明了球面5点猜测。并由此引发了不少相关问题的解决，比如参考这个方法， 美国布朗大学Schwartz教授证明了另外一个难题；近几年相关的成果也不断出现。本报告以球面五点问题为例，简要介绍不等式自动证明的区间分析方法。

侯晓荣： 电子科技大学教授。先后在中国科学技术大学、中国科学院数学所、中国科学院成都计算机应用研究所、宁波大学工作。获1999年度国务院政府特殊津贴。研究兴趣包括机器学习、智能计算、自动推理、自动控制、智能物联网、统计理论及应用等。研究内容涵盖基础理论、工程设计、实现技术等多个层次。发表专著2部、论文100余篇。主持完成国家自然科学基金项目4项、国家973项目子课题3项、国家攀登计划项目子课题1项、国防科工局项目1项、教育部科技重点项目1项、中国科学院重点项目1项等多项。申请国家发明专利10余项等。