At that stage, the system could not handle experts' latest theorems, but it could support formalizing basic material in their fields.

“You know, an expert would come along, and their first question would be like, "Can we do my latest theorem?" And the answer was, "No, but we can do, you know, the basics in your area.”