The NP-complete problem you describe corresponds to automated theorem proving, i.e. searching for a proof of a new mathematical theorem: this is indeed a difficult search problem. Verifying that an existing, human-created proof is correct is a different problem which is definitely tractable.
The real challenge is putting in the grunt-work of formalizing the undergrad math curriculum: one estimate put the required effort at about 140 man-years.
The NP-complete problem you describe corresponds to automated theorem proving, i.e. searching for a proof of a new mathematical theorem: this is indeed a difficult search problem. Verifying that an existing, human-created proof is correct is a different problem which is definitely tractable.
The real challenge is putting in the grunt-work of formalizing the undergrad math curriculum: one estimate put the required effort at about 140 man-years.