Speaker: 侯晓荣，电子科技大学

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

Language: Chinese

Time & Venue: 2024.06.07 10:00-11:00 腾讯会议：448-996-081

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