Just to make it explicit, checking an existing proof is very decidable, given a reasonable programming language. Now getting that proof does pose some practica

Just to make it explicit, checking an existing proof is very decidable, given a reasonable programming language. Now getting that proof does pose some practical difficulties, but it would doubtless be built up by fairly simple proofs derived from user-supplied editing steps; a bit of a pain, but not Halting-complete.