Comment by kurlberg

Recently a lean formalized proof of the Collatz conjecture had exploited bugs in the lean kernel. However, the kernel is fairly small so hopefully it'll be bullet proof soonish.