9 ms·
Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?
by remywang 3mo ago
Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?
- cperciva 3mo agoA counterexample of the form "X cycles to X after N steps" is easy to check. A counterexample of the form "starting with X we keep going up forever" is hard to check in finite time.
- IsTom 3mo agoAnd still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).
- AnimalMuppet 3mo agoYou, sir, have a very different definition of "not particularly large" than I do!
- jonathrg 3mo agoThis feels like saying there are probably hundreds of stars in the universe
- derdi 3mo agoThis was never about the Collatz conjecture itself. If I understand the original discussion correctly (as of a few days ago, not sure if new stuff has come to light), everybody agreed that that framing was just a flashy gimmick. And some Lean maintainers were unhappy about it, since this framing just added noise to the reproducer; they would have preferred a simple proof of False. Nobody ever thought that the disproof might be real.
- paulddraper 3mo agoThis had nothing to do with Collatz and everything to do with a Lean bug. The proof was not actually a proof at all, because it was unsound (despite Lean admitting the proof).
- jojomodding 3mo agoNo, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample.