人机协同证明的时候，设置至少一个数学形式化评审专家很有必要。最近几十个小时尝试证明一个猜想，AI三次声称完成了证明，结果每次都被评审专家找到严重漏洞，诸如循环论证与使用未经证明的假设等等，并且往往隐藏在Lean文件的深处。现在，我看到AI声称证明完毕，所有漏洞已经被修复，心里没有任何波澜。已经构造分析了几千个例子，依然没有反例，但也没有证明猜想，现在有点怀疑我是不是走错路径了，或者猜想本身有问题。
发布于 辽宁
运筹士