It is sometimes asserted that human-readable mathematical proofs that we construct and publish are just informal approximations to the gold standard, which is a completely formal proof in a formal language. The formal proof is supposed to be the real McCoy, the pinnacle of Platonic perfection, which our messy informal proofs try their best to gesture toward.
I seem to recall reading criticisms (of the above assertion) that focused on the enormous size of formal proofs, claiming that they were so large and unwieldy that it would be impossible to write them down in full. If they are so large that we cannot actually produce them or even properly grasp them in our minds, then can we legitimately claim that such fictions are what proofs really are, or strive to be?
Although I feel that I have encountered the above criticism many times, I am having trouble finding an explicit example of someone making this kind of argument in print. The closest thing I have found is A. R. D. Mathias's essay, A term of length 4,523,659,424,929, which discusses a system for set theory due to Bourbaki, and emphasizes the gigantic size of even very simple terms in the system. However, Mathias's criticism is narrowly focused on Bourbaki's system in particular, and he does not take the additional step of arguing that all fully formal proofs are too long to write down, and (thus) cannot in any sense be what mathematical proofs really are, or aspire to be.
In the introduction to the book 18 Unconventional Essays on the Nature of Mathematics, Reuben Hersh recalls the distinction that he made in his earlier book (What Is Mathematics, Really?) between formal proof and "an argument accepted as conclusive by the present-day mathematical community," and mentions the Flyspeck Project to produce a completely formal proof of the Kepler Conjecture. Hersh writes, "I do not know anyone who thinks either that this project can be completed, or that even if claimed to be complete it would be universally accepted as a convincing proof of Kepler's conjecture." What Hersh writes here is close to what I am looking for; on the question of what proofs really are, he clearly favors informal proof over formal proof, and he expresses some skepticism about formal proofs that is related to their size. But he still stops short of arguing that formal proofs of nontrivial mathematical theorems are simply too large and complicated to ever instantiate in the real world.
Is there a better published reference for the argument that (1) formal proofs of nontrivial theorems are intrinsically so huge that they will forever remain figments of our imagination, and (2) therefore we should be skeptical of the role of formal proofs in the justification of mathematical knowledge? I'm imagining that such a reference would likely date from the mid-20th century, since nowadays the existence of computerized proof assistants makes it much harder to argue that fully formal proofs of nontrivial theorems can never be instantiated in the real world.