Hacker News: juhopitkhttps://news.ycombinator.com/user?id=juhopitkHacker News RSShttps://hnrss.org/hnrss v2.1.1Sun, 02 Aug 2026 23:34:30 +0000<![CDATA[New comment by juhopitk in "Postmortem for Kernel Soundness Bug #14576"]]>"A soundness bug in the Lean kernel (#14576) was reported and fixed during the week of July 27. [...] On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576."

]]>Sat, 01 Aug 2026 18:32:20 +0000https://news.ycombinator.com/item?id=49137061juhopitkhttps://news.ycombinator.com/item?id=49137061https://news.ycombinator.com/item?id=49137061<![CDATA[Postmortem for Kernel Soundness Bug #14576]]>Article URL: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/

Comments URL: https://news.ycombinator.com/item?id=49137060

Points: 161

# Comments: 62

]]>Sat, 01 Aug 2026 18:32:20 +0000https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/juhopitkhttps://news.ycombinator.com/item?id=49137060https://news.ycombinator.com/item?id=49137060