MarchBeta2087 在【慢讯】Lean 4 出现严重 Bug：一个“反例”炸出了漏洞中发帖2026 年 7 月，Ramana Kumar 声称通过 AI 发现了 Collatz 的反例

MarchBeta2087 在【慢讯】Lean 4 出现严重 Bug：一个“反例”炸出了漏洞中发帖

2026 年 7 月，Ramana Kumar 声称通过 AI 发现了 Collatz 的反例。然而，这个反例是无效的：它利用了 Kernel 内核的一个漏洞。 
 [Screenshot_2026-08-07-00-12-48-145_com.android.chrome] 
[Screenshot_2026-08-07-00-15-37-504_com.android.chrome] 
GitHub 用户 Kiran Gopinathan 提交的 Issue： 
 [Screenshot_2026-08-07-00-18-30-037_com.android.chrome] 
[Screenshot_2026-08-07-00-18-42-567_com.android.chrome] 
Lean 4 v4.32.2 更新日志。可以看到这个 Bug 已经被修复。 
 [Screensh...