Computers tend to be pretty bad at NP-hard problems, and even the “simple” task of determining whether or not a statement of propositional logic is a contradiction is NP-complete… formalized proofs are, in general, going to be bloody huge computational nightmares.
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.
Computers tend to be pretty bad at NP-hard problems, and even the “simple” task of determining whether or not a statement of propositional logic is a contradiction is NP-complete… formalized proofs are, in general, going to be bloody huge computational nightmares.
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.