Is there a universal math proof verification program than can verify every finite purported math proof? For some axiom systems, we can verify candidate proofs. For example Mizar.
Is there a universal language we can write proofs in, so that the axioms are included in the proof, along with every single step in complete detail, so that some universal verifier (Turing machine) can decide its correctness? Assume proofs are finite in length.
(I believe this is similar to asking "Can every math proof be written in Metamath?")
Basically instead of hard-coding the axiom system into the verifier, I want the axioms as part of the input to the verifier, for all possible axiom systems.

Turing machines have Universal Turing machines that compute all other turing machines.
Turing machines and math proofs seem to be closely related (See Curry-Howard correspondence and the time- and space- hierarchies from Computer Science showing up in higher-order-logic via Descriptive Complexity).
So there may be some analogous universal math axiom system that can describe all other systems.
 A: If you fix on some logic, e.g., first-order logic and as is usual require the axiom system to be a recursive set, then you can design a machine that takes as input a purported proof $\Pi$ and a code $\cal A$ for a function that decides whether a formula is an axiom and tests whether $\Pi$ is a valid proof from the axioms in $\cal A$. Generalising, you could come up with a fancier machine that took as input a purported proof in any reasonable deductive sstem and a function that decomposes the proof into steps and decides whether each step is valid. Systems along these lines have been implemented and are called logical frameworks. Metamath is one such system. However, I don't think any such system enjoys any very interesting universal property: there is no useful sense in which they describe the systems that they model.
However, all this depends on our logic being tractable to computation. In the logic whose language is the language of natural number arithmetic and whose axioms are all true statements about the natural numbers, there is no possibility of providing a verifier.
A: There's some discussion in the comments about what exactly the question means, so I'll try to give an answer that covers a variety of possible meanings.  Here's some helpful terminology.  A proof system is:

*

*complete if every statement that is true under all interpretations can be proved in the system.

*sound if every statement that can be proved in the system is true under all interpretations.

*effective if there is an algorithm that can correctly detect whether a given string of symbols is a correct proof.

Now whether or not there is proof system like you're asking for depends on exactly what you want, and which logical framework you want to work in.  For example, first-order logic does have a complete, sound, effective proof system (in fact, there are several).  On the other hand, it follows from the incompleteness theorems that second-order logic (with full semantics) does not have a complete, sound, effective proof system.
I feel like I should note that getting a sound and effective proof system is trivial - just declare that no string of symbols is a proof. Completeness, or at least something like it, is thus highly desirable.
I also think I should point out that despite having a complete, sound, effective proof system, there is not an algorithm for determining whether or not a given statement is a theorem from some axioms, but there is an algorithm which, given a statement and some reasonably-presented list of axioms, will return TRUE if the statement can be proved from the axioms, and otherwise will run forever.  The terminology here is that first-order logic is semidecidable.
