题目：不等式自动证明的区间分析方法——以球面五点问题为例
时间：2024年6月7日上午10:00–11:00
地点：腾讯会议448-996-081
主讲人简介：
侯晓荣，1997年晋升研究员。先后在中国科学技术大学、中国科学院成都计算机应用研究所、宁波大学工作，现为电子科技大学教授。获1999年度国务院政府特殊津贴，主持完成国家级课题10余项。研究兴趣包括自动推理、自动控制、机器学习、智能计算、智能物联网及应用等。理论方面：主要利用各种数学工具描述系统的动静态特性，研究建模、预测、优化决策及控制；以信号处理、人工智能、控制论、计算机技术为基础，研究信息的采集、处理、特征提取、模式识别与分析、智能系统的设计。应用方面：将控制技术、智能技术、计算机技术、网络技术和现代检测技术相结合，形成各种新型的控制器和控制系统。研究内容涵盖基础理论、工程设计、实现技术等多个层次。
内容简介：
在数学的各个分支领域，人们希望用相对简单而易于控制的对象去把握复杂的事物，于是产生了不等式。不等式在数学研究中发挥着显著的作用。在吴先生的倡导并身体力行下，数学机械化领域蔚然已成大气。吴先生对不等式类问题的算法化和机械化问题多有研究，并多次在数学机械化的各类会议中提及不等式自动证明的困难性。以往相关的工作，集中于处理半代数集问题，其效率主要体现在低维以及约束条件较简单的问题上。面对如“球面5点”之类问题，尽管该问题实质仍是半代数集问题，但变量个数较多、约束关系较复杂，这些方法仍一时难以处理。球面5点问题可以追溯到1931年，是一个长期悬而未决的难题。有大量的文献研究此类问题，Smale把这类问题列为21世纪的数学问题之一。针对此类不等式的自动证明，我们提出了区间分析的方法，用这个方法证明了球面5点猜测。并由此引发了不少相关问题的解决，比如参考这个方法，美国布朗大学Schwartz教授证明了另外一个难题；近几年相关的成果也不断出现。本报告以球面五点问题为例，简要介绍不等式自动证明的区间分析方法。
