After a year of work, Kevin Hartnett's team was translating statements of theorems published in leading pure-mathematics journals during the current decade into a formal software language, and the project was becoming viable.

“And, uh, and we've spent a year working on this now, and it now is sort of, it's becoming viable. We're taking, uh, theorems published in, you know, the top pure maths journal, uh, this decade, and we're trying to translate just the statements of the theorems, uh, into the language of the software.”