4 ms·
Why is it all in the kernel?
- Nzen 3mo agoLaurence 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 https://github.com/xrchz/CollatzLean Paulson (mercifully?) did not link to Kumar's repository or paper [1] [1] https://websim.com/@BookwormKevin/collatz-conjecture-simulation 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/S0747717186800025?via%3Dihub https://www.sciencedirect.com/science/article/pii/S074771718... DOI 10.1016/S0747-7171(86)80002-5