Tom Hales advocated carrying out the theorem-statement formalization project in 2017, but it was too difficult then.

“Uh, in fact, it was somehow not quite viable at that moment. You know, Ha- Hales pushed for, Hales pushed for it to be happening in twenty seventeen. Uh, and it was somehow too difficult to do in twenty seventeen.”