Post #4200216

2026-07-28 13:51 UTC

References: https://github.com/leanprover/lean4/pull/14577 the main issue https://github.com/ammkrn/nanoda_lib/pull/22 the nanoda PR from yesterday that (apparently independently (!!!)) catches the problem on their side https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/with/613135216 Lean Zulip discussion

Replies (1)

@yforster@types.pl 2026-07-28 16:15

@mevenlennonbertrand@lipn.info it's a very nice story, but we should mention that the human who let the AI agent loose is Ramana Kumar (https://dblp.org/pid/30/8321.html) and I cannot possibly imagine Ramana really thought that this is a disproof of the collatz conjecture

Open ##4231609