This back-and-forth makes me wonder, is it possible to write proofs about proofs? e.g., you cannot prove this result without logarithms or there must exist a proof that involves prime factors?
I suppose at least some proofs vaguely like that are possible because Gödel's incompleteness theorem is one, although I suspect that that same theorem puts some constraints on these "metaproofs."
Yep, I took several metamathematics classes at UCLA! Mostly on proof theory, but also analyzing metamathematical results (like Godel's theorems, Henkin construction, and so on).
I suppose at least some proofs vaguely like that are possible because Gödel's incompleteness theorem is one, although I suspect that that same theorem puts some constraints on these "metaproofs."