为何Isabelle的sos方法能证明明显错误的引理？

你遇到的情况并非Isabelle核心证明机制的问题，而是对sos方法的适用场景和底层实现的误解：

• sos方法的定位偏差
  sos（平方和）是专门用来证明实系数多项式非负性的工具，比如证明x² + 1 ≥ 0这类命题——它通过将目标多项式分解为多个平方项的和来完成证明。它并不适合直接用来验证等式，尤其是明显矛盾的等式。

• 数值求解器的精度缺陷
  sos依赖外部数值求解器（如CSDP），这类工具使用浮点数运算，存在固有精度限制。尽管8/7和2的差值看起来很大，但求解器在内部处理时，可能因异常的精度丢失或判定逻辑偏差，错误地判定矛盾等式成立。

• Isabelle的证明逻辑
  Isabelle只会检查你提供的证明步骤是否符合逻辑规则，不会主动验证引理本身的语义合理性。当sos返回“证明成功”时，Isabelle就会认为子目标已完成证明，不会额外校验引理是否符合现实语义。

• 验证等式或算术命题时，应该用auto、simp、arith这类专门处理等式推理的方法。比如你的例子里，把sos换成auto，Isabelle会直接报错，明确指出矛盾。
• 只在需要证明多项式非负性时使用sos，比如证明(r-1)² ≥ 0这类符合其定位的命题。

内容的提问来源于stack exchange，提问作者Ze-Nan Li