Ciro Santilli @cirosantilli 37

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.

There are to ways in which the Collatz conjecture can fail:These are the only two options because if any sequence has an upper bound, it must sooner or later repeat an element, leading to a cycle.

This section is about benchmarks designed to test mathematical reasoning.

Bibliography: