Comment by lseplot

https://github.com/anthropics/fermats-last-theorem/blob/main...

  status: "self-assessed"

13 million lines of Lean, where the Lean and Nanoda kernels missed the Collatz hack.

Fable, please translate to HOL-light. Make no mistakes. You are doing great!