The Completeness Theorem in first-order logic states that any mathematical validity is derivable from axioms. Hence, any informal mathematical proof (which is rigorous) can be translated into a formal proof in any reasonable proof system. However, this formal proof may be larger than the informal, natural-language proof.

Is there any proof system with the property that all known natural-language proofs have formal proofs with only a constant or polynomial blow-up in the proof length?