No, because a proof (especially a human-constructed proof) is a finite object built out of basic pieces. The only question as to the validity of a proof is whet

No, because a proof (especially a human-constructed proof) is a finite object built out of basic pieces. The only question as to the validity of a proof is whether the basic pieces have been fit together according to the established rules of the game. We don't have to have any notion of "execution" of a proof to verify that its construction is valid. Let me put it this way. I tell you that I can make apple juice if you give me an apple and a juicer. Do you have to give me anything to believe me? Several researchers have indeed put together a theory of "execution" of a proof; see for instance Prof. Frank Pfenning's research program on logic-based process calculi. These theories tend to have the common theme of execution as normalization -- the chosen mode of execution actively changes and evolves the proof structure until it reaches a terminal form, usually one with a particularly simple logical structure. Cut elimination is a central theme: any logical system worth calling "computational" (one argues) will support cut elimination, allowing you to replace a proof with steps like `A -> B, B -> C |- A -> C` with a direct proof of `A -> C` that does not use the intermediate hypothesis `B`. But we're not doing that when we're verifying a proof. We're looking at the finite, static structure of a proof term, and checking that it was put together legally.