Ciro Santilli @cirosantilli 37

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:

Quick list: x.com/AlexKontorovich/status/1997051032384446629