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 2 hours ago | parent | next [-]

A 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 2 hours ago | parent [-]

And still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).

▲

AnimalMuppet an hour ago | parent [-]

You, sir, have a very different definition of "not particularly large" than I do!

	▲	Sharlin 21 minutes ago \| parent [-]
		To be fair, BB(40) is smaller than almost all positive integers.

▲

paulddraper 37 minutes ago | parent | prev | next [-]

This had nothing to do with Collatz itself and everything to do with a Lean bug.

The proof was not a proof because it was not sound, even though Lean admitted the proof.

▲

derdi an hour ago | parent | prev [-]

This 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.