2006年发表的一篇关于"双希格斯双重态模型"稳定性的论文，给物理学界带来了震撼。这篇论文因清晰的数学结构和频繁引用而被认为安全可靠，不过这个错误在它发表后的二十年里一直没有被发现。巴斯大学的研究员约瑟夫·托比-史密斯把这篇论文用Lean进行了形式化验证，结果发现了一个逻辑错误。 约瑟夫·托比-史密斯是在推进一个名为PhysLib的项目时发现这个错误的。他试图把已发表的物理学研究成果转化为可供计算机验证的形式化代码，类似MathLib数据库。他认为这篇论文看起来很可靠，没什么问题，把这个过程描述为“一次打勾的例行工作”。 然而，当他用Lean验证这个论文时，得到了一个意外的结果。Lean告诉约瑟夫·托比-史密斯，这篇论文的核心定理在逻辑上站不住脚。具体来说，原论文作者断言条件C对势能稳定性是充分的，即满足条件C就能保证稳定。然而，托比-史密斯构造出了一个反例：一个满足条件C却并不稳定的势能。这个反例被Lean完整验证，并判定原论文的核心定理是可证伪的错误。 这次发现展示了形式化验证与传统同行评审之间本质差异。传统同行评审依赖专家直觉和经验，在面对高度抽象数学推导时很容易忽视跳跃步骤和隐含假设。而形式化语言如Lean则要求每一个推理步骤都必须严格证明，不允许任何逻辑跳跃和隐含假设。一旦某个步骤无法被系统接受，整条推理链就会断掉。 帝国理工学院数学家凯文·巴扎德指出，在数学领域积累足够多的形式化训练数据依然是一项艰巨工程。托比-史密斯也提到物理学家写作习惯与数学家不同，常常会省略一些细节步骤导致错误产生。 虽然这次发现直接影响相对有限，因为大量后续研究只采用了势能四次项部分而不是完整势能分析。但这并不影响它象征意义更加突出：几乎没有嫌疑的论文在第一次接受形式化验证时就暴露了根本性错误。 这个问题也引发了物理学界关注：还有多少未经历过这种级别的审查？