Lean repository linked
Almost all orbits of the Collatz map attain almost bounded values
arXiv:1909.03562 · arXiv
Lean formalisations (1)
gotrevor/tao-collatz at 95a7172bb253
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.