The question probably leads easily to anachronistic answers.
My understanding is that according to current scholarship Hume (and Descartes and Locke) had views about inference that are opposed to the modern more "formalistic" or deductive view.
Descartes, Locke & Hume knew about the formalistic view through the earlier scholastic understanding of deduction, according to which an argument is valid because the premises and the conclusion have the right (propositional) form. This idea comes from Aristotle's syllogistics and we have our version of it also. According to this view computer generated proofs are basically on a par with human generated proofs.
Hume on the other hand inherited his views about inference from Descartes and Locke. According to all of them during inference your "mind" (or some cognitive faculty) moves from one idea to the next. (My understanding is that they don't have much use for propositions as a special category, propositions are collections of ideas for them.)
For example, a demonstrations of the Pythagorean theorem is an attempt to find a chain of ideas that makes it possible to recognize (or to intuit) that the ideas "square of the hypotenuse" and "sum of the squares of the other two sides" are in a certain relationship (in this case, are equivalent). (See Owen for more details.)
So I don't see how on this view one could say, as you do, that computer generated proofs are "relations of ideas par excellence", because they are symbols on a paper.
Descartes specifically objected that in formal deduction one can deduce truth from falsity and falsity from falsity. For Descartes the point of a demonstration is to distinguish truth from falsity, and for this you need to have the content of the inference in mind.
For him the point of inference is to give you new knowledge. So formal deduction is in this sense useless because firstly you gain knowledge by deduction only if the truth of the premises is already known, and secondly because you don't gain new knowledge since the conclusion is already contained in the premises.
No doubt this view is very problematic from a modern perspective, but according to Owen this was Descartes' view. (Ian Hacking even argued that Descartes had no conception of proof at all!)
Hume inherited basically this same view through Locke. (Of course Descartes and Locke had different views about the origin of ideas.)
See Hume's Reason by David Owen for more details.