Ciro Santilli @cirosantilli 40

The Collatz function is not very elegant in that the odd $3n+1$ case is always even because $n$ is odd, so it is always predictably followed by a division by two. This is not the case for the even case, where the result can be either even or odd.

A much more elegant formulation is to immediately also divide by two when the number is odd:

Here is a specific minimal example of how to use mathlib4: proofassistants.stackexchange.com/questions/2526/how-to-run-lean4-with-mathlib-manually/5299#5299

We define an "integer algorithm" as an algorithm that takes integer inputs and produces integer outputs.