Just read the following line in algorithms book by Dasgupta, Papadimitrious and Vazerani,
the task of finding a proof for a given mathematical assertion is a search problem and is therefore in NP (after all, when a formal proof of a mathematical statement is written out in excruciating detail, it can be checked mechanically, line by line, by an efficient algorithm).
I'm not a CS theorist by any stretch, but my understanding is that $NP$ can be informally described as problems with an algorithm $C(I,S)$ where $I$ is the problem statement and $S$ is a solution, such that $C(I,S)$ returns true if $S$ is a solution to $I$ and false otherwise and does so in $O(n^{|I|})$ time.
The statement in the book sounds like they measure efficiency in terms of $O(n^{|S|})$. Yes, given a proof ($S$), I can verify it line by line, but that proof might be exponential in the length of the problem statement ($I$).
Am I misunderstanding something?