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).