In a set-theoretic system using first-order logic, every proof could be written as a goal followed by a finite sequence of sentence where each one is justified by an axiom or previously established sentence and the last line is the goal. Computers can easily verify proofs like these using the rules of first-order logic.


In dependent type theory, proofs come in the form of programs, and you know your proof is correct if it can be compiled (or type-checked).


Do there exist logics/foundations where rigorous proofs can not be checked by computers? Or where a checking program might never terminate for a correct proof?



Are there logical systems where formal proofs are not computer verifiable?
There are logical systems whose formal proofs are not computer verifiable. One such example is [infinitary logic](https://en.wikipedia.org/wiki/Infinitary_logic) in which logical statements can be infinitely long, and a specific statement in a proof may require infinitely many premises to be checked. Such logical systems have their value in studying various aspects of foundations of mathematics, but are not normally considered to properly reflect the actual human activity of proving mathematical statements.


All logical systems (first-order logic, higher-order logic, type theory, etc.) whose purpose is to capture the notion of proof as done in practice, have machine verifiable proofs. The formal property needed here is [semidecidability](https://en.wikipedia.org/wiki/Decidability_(logic)#Semidecidability).


**Supplemental:** Noah Schweber points out another example of a formal logic which is not comuputer-verifiable. Namely, we could take as the axioms of our logical system all statements that are *true* in a certain class of mathematical structures. Depending on what this class of structures is, we might end up with a non-computable set of axioms, which then presents a problem for verifiability. Here are some examples:


1. If we take ordinary Peano arithmetic and add to it as axioms all true sentences, we get a non-verifiable system by Gödel's incompleteness.
2. If we take all equations in the language of a group (so we can use the group unit, operation and inverses) which hold in every group, we will get a set of equations that is already generated by the standard axioms for a group theory, and therefore semidecidable (computer-verifiable).


