Tom Hales's ideas about formalizing theorem statements took years to become reality.

“And I would imagine that in a year's time, we're gonna be far more than twenty percent through. So some- so, so Hales had these ideas which have taken years, uh, to become real.”