You don't need to prove that Peano arithmetic is consistent! You just need to prove that the theorem prover doesn't contain any bugs, i.e. that it correctly imp

You don't need to prove that Peano arithmetic is consistent! You just need to prove that the theorem prover doesn't contain any bugs, i.e. that it correctly implements peano arithmetic. That's a much lower bar, and theorem provers have verified themselves in the past.