Laurence Paulson laments a bug that fooled Ramana Kumar using both Lean proof system and the Nanoda (plugin ? library ?) into thinking that he found a counterexample to the famous Collatz Conjecture [0]. It sounds like Kumar or someone extended the Lean software to postulate that a certain style of proof is true and Kumar's larger proof hallucinated a class of numbers that enter a cycle in the Collatz sequence.

[0] https://github.com/xrchz/CollatzLean Paulson (mercifully?) did not link to Kumar's repository or paper [1]

[1] https://websim.com/@BookwormKevin/collatz-conjecture-simulat... this is a visualization of the Collatz sequence of numbers that is conjectured - but not proven - to always terminate at 1.

Paulson laments this as there are ways of building up the rules from axioms (program objects?), but it is really tedious. He recounts crafting a "system of combinators" (in 1986) that one could build on to express recursive functions.

[2] https://www.sciencedirect.com/science/article/pii/S074771718... DOI 10.1016/S0747-7171(86)80002-5