近日，北京邮电大学郁文生教授团队与北京大学王龙教授团队借助于 GPT-6 Astra，对控制理论中的一个公开问题——五阶区间族严格正实综合问题——给出了正面解答，并在 Lean 4 中完成了形式化验证。相关代码已经通过完整构建和校验。至此，这一长期悬而未决的理论难题获得了可由计算机内核逐步核验的严格证明。

与将已有数学证明转写成形式化代码不同，本研究面对的是一个尚待解决的公开问题。AI不仅参与了证明的形式化表达，也为研究路线探索、复杂情况分析和论证条理组织提供了支持。这项工作体现了AI在促进控制理论关键问题上取得实质性进展的可能性。

五阶区间族的严格正实综合问题

实际控制系统的参数通常无法精确测量，往往只能确定其变化范围。用数学语言描述时，系统的特征多项式的每个系数都是未知的，只知道上下界。所有可能的系数组合共同构成一个五阶区间多项式族。

如果这个多项式族中的每一个成员都满足 Hurwitz 稳定性，也就是所有零点均位于复平面的开左半平面，就称该多项式族为鲁棒 Hurwitz 稳定。

五阶区间多项式族的严格正实综合问题是：如果整个区间族A(s)都稳定，是否一定存在一个固定的实系数五阶多项式b(s)，使得对于区间族中的每一个多项式a(s)，都有

b(jw)/a(jw) > 0, for all w in R

这里最重要的要求是，b(s)必须是一个对整个区间族都有效的公共分子，不能随着具体的a(s)改变。

“综合问题”不同于通常的严格正实性检验。检验问题是在分子和分母都已给定后，判断某个传递函数是否严格正实；综合问题则要从整个不确定性集合出发，证明一个公共分子存在，并保证它同时适用于无穷多个可能的系统模型。

严格正实性与系统的无源性、稳定性和能量耗散性质密切相关，在绝对稳定性、鲁棒控制、自适应控制和系统辨识等领域具有重要作用。因此，寻找整个不确定系统族的公共严格正实分子，是一个兼具理论意义与工程背景的问题。

一个延续数十年的理论问题

1978年，苏联数学家 Vladimir Kharitonov 证明，一个实区间多项式族是否全部稳定，只需检查四个特殊的顶点多项式。Kharitonov 定理使原本需要面对无穷多个多项式的稳定性问题，转化为有限检验，成为参数不确定系统鲁棒稳定性研究的重要里程碑。

在稳定性研究的基础上，人们进一步提出了更困难的严格正实综合问题：不仅要判断整个多项式族是否稳定，还要为它寻找一个统一适用的公共分子。该问题1987年由美国控制理论学者Dasgupta和Bhagwat在研究鲁棒自适应控制时提出，曾引起包括国际自动控制联合会前主席、澳大利亚科学院前院长Anderson 教授在内的多位著名控制理论专家的关注。

1990年，Brian D. O. Anderson、Soura Dasgupta、Pramod Khargonekar、Frantisek Kraus 和 Mohamed Mansour 系统研究了鲁棒严格正实函数的刻画与构造，并证明了四阶稳定区间多项式族具有公共严格正实分子的结论。

1993年，以色列学者A. Betser 和 E. Zeheb 指出，Anderson 等人证明中使用的一个线性规划条件并不是公共严格正实分子存在的必要条件。他们给出了一个能够完成严格正实综合、但相应线性规划问题没有解的例子。这说明Anderson等人的证明是错误的，但A. Betser 和 E. Zeheb并没有否定四阶鲁棒严格正实的存在性本身。

2001年，郁文生和王龙构造性证明了四阶稳定区间多项式族鲁棒严格正实综合的存在性，确认了 Anderson 的原始论断。该成果发表于 IEEE Transactions on Circuits and Systems I，题为 Anderson’s Claim on Fourth-Order SPR Synthesis is True。

同一时期，郁文生和王龙还解决了五阶多项式凸组合的鲁棒严格正实综合问题。随后，郁文生、王龙和 Jürgen Ackermann 将凸组合情形推广到任意阶，证明了由两个固定多项式形成的稳定多项式凸组合具有公共严格正实分子。

然而，多项式凸组合与区间多项式族存在本质区别。凸组合只沿一个参数方向变化，而区间多项式族中的多个系数可以彼此独立变化，形成更复杂的高维不确定性集合。因此，任意阶凸组合问题的结论不能直接用于区间多项式族。

自四阶区间多项式族问题于2001年获得严格证明后，五阶区间多项式族的相应问题一直没有取得突破。

五阶区间族问题获得正面解答

本次工作证明：对于任意稳定的五阶区间多项式族A(s)，一定存在一个固定的五阶多项式 b(s)，使得b(s)/a(s)对整个区间族(for all a(s) in A(s))和所有实频率w均具有严格为正的实部。

面对由连续系数和连续频率共同构成的无穷多约束，研究团队首先寻找其中能够统一描述问题的数学结构，再将无穷条件逐步转化为可以分析和排除的有限情形。GPT-6 Astra 帮助研究人员开展大规模探索、比较不同证明路线，并处理大量相互关联的中间命题。研究团队在此基础上完成了数学框架选择、关键结论判断、定义校验和完整证明组织。

这一过程最终形成了从问题定义到主定理的完整逻辑链条，并进一步转写为 Lean 4 可以检查的形式化证明。

完整证明在 Lean 4 中通过机器核验

正式证明包含约7000行 Lean 源码、66个数学模块和431条显式定理及引理，覆盖问题定义、稳定性基础、频域条件、公共分子的存在性以及最终结论等内容。

完整代码已经在独立环境中通过构建与校验。

验证过程表明，主定理不依赖未完成证明占位符或额外假设。Lean 内核对证明中的每一步类型和逻辑关系进行了核验，从而使整个证明具有可检查、可追踪和可复用的形式。

从验证已知结论到参与解决开放问题

本课题的重要意义在于，AI参与研究的对象并非一道已有标准答案的问题，也不是一篇已经完成的论文，而是一个具有明确研究历程、经历过错误证明并长期没有解决的科学难题。

对于这类问题，困难不仅在于完成大量计算，更在于找到正确的数学表述、识别真正的关键障碍，并把零散发现和中间结果组织成能够覆盖全部情况的完整证明。AI可以同时考察更多候选路线，帮助整理大量相互依赖的中间结果，并迅速发现局部论证中的矛盾或遗漏。

形式化证明则为这种研究方式提供了严格的质量控制。AI 可以辅助完成证明步骤和生成代码，但最终每一步都必须通过 Lean 内核的检查。科学家负责问题选择、科学意义判断和整体路线把关，AI负责扩大探索范围并提高迭代效率，证明助手负责执行严格核验，三者形成相互补充的研究模式。

这一模式提示我们，AI 在人类正确引导下对科学研究的价值不仅是“更快地完成已有任务”，还可以帮助人类进入过去因复杂度过高而难以充分探索的区域。

对高阶严格正实综合问题的展望

我们已经解决了任意阶多项式凸组合的鲁棒严格正实综合问题。然而，对阶数大于等于六的区间族相应结论目前仍未获得。

尽管五阶问题的解决对研究六阶及更高阶区间族有一定启发性，但并不意味着高阶结论已经自然成立。随着阶数增加，可能出现的临界情况和不同系数之间的组合关系会迅速增多，五阶证明中依赖阶数限制的部分也不能直接照搬。我们目前正在尝试对六阶情形的形式化证明，任意阶区间族鲁棒严格正实综合问题是具有极大挑战性的。

相关链接

GitHub 仓库：https://github.com/dgjszy/quintic-spr-proof

重要文献

·       V. L. Kharitonov, The Asymptotic Stability of the Equilibrium State of a Family of Systems of Linear Differential Equations, Differentsial’nye Uravneniya, 14(11), 1978, 2086–2088。

·       S. Dasgupta and A. S. Bhagwat, Conditions for Designing Strictly Positive Real Transfer Functions for Adaptive Output Error Identification, IEEE Transactions on Circuits and Systems, 34(7), 1987, 731–736。DOI: 10.1109/TCS.1987.1086198

·       B. D. O. Anderson, S. Dasgupta, P. Khargonekar, F. J. Kraus and M. Mansour, Robust Strict Positive Realness: Characterization and Construction, IEEE Transactions on Circuits and Systems, 37(7), 1990, 869–876。DOI: 10.1109/31.55062

·       A. Betser and E. Zeheb, Design of Robust Strictly Positive Real Transfer Functions, IEEE Transactions on Circuits and Systems I, 40(9), 1993, 573–580。

·       Wensheng Yu and Long Wang, Anderson’s Claim on Fourth-Order SPR Synthesis Is True, IEEE Transactions on Circuits and Systems I, 48(4), 2001, 506–509。DOI: 10.1109/81.917990

·       Long Wang and Wensheng Yu, Robust SPR Synthesis for Low-Order Polynomial Segments and Interval Polynomials, Proceedings of the 2001 American Control Conference, Vol. 5, 3612–3617。

·       Wensheng Yu and Long Wang, Robust Strictly Positive Real Synthesis for Convex Combination of the Fifth-Order Polynomials, Proceedings of International Symposium. on Circuits and Systems, 2001, Vol. 1, 739–742。

·       Wensheng Yu and Long Wang, Robust Strictly Positive Real Synthesis for Convex Combination of Sixth-Order Polynomials, 2003 American Control Conference, 3840–3845。

·       Wensheng Yu, Long Wang and Jürgen Ackermann, Solution to the General Robust Strictly Positive Real Synthesis Problem for Polynomial Segments, European Control Conference, 2003, 1744–1749。

·       Wensheng Yu, Long Wang and Jürgen Ackermann, Robust Strictly Positive Real Synthesis for Polynomial Families of Arbitrary Order, Science in China Series F: Information Sciences, 47(4), 2004, 475–489。DOI: 10.1360/03yf0053

支持单位：