[camjw]

> a language for defining relationships between quantities

Could you expand on this? I don't see maths as a language for quantities specifically (i.e. what does symmetry have to do with quantities).

> just too tedious (but not impossible) for a human being to work through the proof.

Already happened with the four colour theorem arguably.