Hi, I'm not sure I understand what your question really is - frankly, I don't think that there is anything left to formalize about the principle of covariance in GR - but I hope that I can be of help nevertheless. Let me just state some remarks:

• "I've read that the principle of general covariance in general relativity is best understood as a gauge symmetry with respect to the diffeomorphism group".

The problem with this statement is that "gauge transformation" in a gauge theory means "a transformation of the mathematical model that does not have any measurable/observable effect". In this sense the existence of gauge transformations means that the mathematical model is redundant, there are degrees of freedom that are not observable. In general relativity a diffeomorphism represents a change of the reference frame. This is of course "observable" in the sense that observers living in different reference frames report different observations of the same event. So I'd say that this analogy is at least as misleading as it is helpful.

You can find more about this on the webpage of Ray Streater here: Diff M as a gauge group.

• "the link between this and the notion of manifest covariance is not obvious to me."

"Manifest" simply means that the covariance of an equation is easy to see (for an educated human), it does not have any deeper meaning.

• "Physicists have a "principle of general covariance" which basically states that physical laws (and in particular, physical quantities) can be stated in a form which is somehow coordinate-independent. The paradox is, such "coordinate-independent" quantities and equations are frequently stated in terms of (admittedly, arbitrary) coordinates!"

I'm not sure I understand what the paradox is. Let's say you sit in a train and pour yourself a cup of coffee. You report: "both the cup and the coffeepot don't move, therefore the coffee ends up in the cup". Let's say I observe this standing at a railroad crossing , I'll report "both the cup and the coffeepot move with 30 km/h to the east, therefore the coffee ends up in the cup". The principle of general covariance says that the event "the coffee ends up in the cup" needs to be a scalar, since all observers will agree on the fact. And the velocity of the cup and the coffeepot in the west-east direction needs to be a vector because all observers will disagree about it according to the relative velocities of their frames of reference.

So, in general relativity, we say that

a) every specific choice of coordinates of (a patch of) spacetime corresponds to an observer, who can observe events and tell us about his observations,

b) given these observations we can predict what every other observer will report by applying the diffeomorphism that takes one set of coordinates to the other set of coordinates to the observations.

The principle of general covariance says that every physical quantity has to transform in a way that we don't get an inconsistency between what we predict what another observer reports and what he actually reports. If you report that the coffee ends up in the cup, and I report that the coffee ends up on you because in my reference frame the cup moves with a different velocity than the coffepot, the theory is in trouble.

More about general relativity, the principle of general covariance and the "hole argument" of Einstein can be found on the page spacetime on the nLab.

Hi, I'm not sure I understand what your question really is - frankly, I don't think that there is anything left to formalize about the principle of covariance in GR - but I hope that I can be of help nevertheless. Let me just state some remarks:

• "I've read that the principle of general covariance in general relativity is best understood as a gauge symmetry with respect to the diffeomorphism group".

The problem with this statement is that "gauge transformation" in a gauge theory means "a transformation of the mathematical model that does not have any measurable/observable effect". In this sense the existence of gauge transformations means that the mathematical model is redundant, there are degrees of freedom that are not observable. In general relativity a diffeomorphism represents a change of the reference frame. This is of course "observable" in the sense that observers living in different reference frames report different observations of the same event. So I'd say that this analogy is at least as misleading as it is helpful.

You can find more about this on the webpage of Ray Streater here: Diff M as a gauge group.

• "the link between this and the notion of manifest covariance is not obvious to me."

"Manifest" simply means that the covariance of an equation is easy to see (for an educated human), it does not have any deeper meaning.

• "Physicists have a "principle of general covariance" which basically states that physical laws (and in particular, physical quantities) can be stated in a form which is somehow coordinate-independent. The paradox is, such "coordinate-independent" quantities and equations are frequently stated in terms of (admittedly, arbitrary) coordinates!"

I'm not sure I understand what the paradox is. Let's say you sit in a train and pour yourself a cup of coffee. You report: "both the cup and the coffeepot don't move, therefore the coffee ends up in the cup". Let's say I observe this standing at a railroad crossing , I'll report "both the cup and the coffeepot move with 30 km/h to the east, therefore the coffee ends up in the cup". The principle of general covariance says that the event "the coffee ends up in the cup" needs to be a scalar, since all observers will agree on the fact. And the velocity of the cup and the coffeepot in the west-east direction needs to be a vector because all observers will disagree about it according to the relative velocities of their frames of reference.

So, in general relativity, we say that

a) every specific choice of coordinates of (a patch of) spacetime corresponds to an observer, who can observe events and tell us about his observations,

b) given these observations we can predict what every other observer will report by applying the diffeomorphism that takes one set of coordinates to the other set of coordinates to the mathematical gadgeds that represent observable entities/effects.

The principle of general covariance says that every physical quantity has to transform in a way that we don't get an inconsistency between what we predict what another observer will report and what he actually reports. If you report that the coffee ends up in the cup, and I report that the coffee ends up on you because in my reference frame the cup moves with a different velocity than the coffepot, the theory is in trouble.

More about general relativity, the principle of general covariance and the "hole argument" of Einstein can be found on the page spacetime on the nLab.