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:

This one focuses on improving speed of important numerical algorithms as compared to popular implementations.

The general pattern can be seen by observing the optimization of: algotune.io/aes_gcm_encryption_anthropic_claude-opus-4-1-20250805.html This shows the chat that the system had.

They define an OS interface to edit files and run right on the prompt, and tell at each stage how many credits are left for a given API and what the speedup was. Amazing. Each task has a $1 budget per provider. Then their software parses commands out of the LLM output and sends formatted responses back. Quite amazing that it works at all.

All pieces of code seem to be in Python, and the speedups come mainly from using more advanced external computing libraries, like compiling with Cython or using faster external libraries that are pre-compiled, or more parallel. So it is not that impressive from a purely algorithmic point of view, but it is not bad either.

Correctness is checked automatically by comparing the optimized solution to the original non-optimized one likely for certain inputs.