Hume's fork divides knowledge of the world into:
How would Hume classify computer generated proofs? On one hand they are relations of ideas par excellence, on the other hand they require a mechanical procedure to be generated, and some of them are too complex for a single human to grasp.
It is helpful to distinguish two questions here: one logical and the other epistemological. If you ask, what is the logical status of a proffered deductive proof of some proposition, then it is either valid or not. It doesn't matter whether the proof was generated by a human mind, a computer, or an explosion in a print factory.
But often, we are interested in the epistemological question: how can we be sure this proof is correct? There are plenty of valid proofs that are very difficult to comprehend: for example, few people know enough math to understand the proof of Fermat's last theorem. Also, there are proofs of theorems that are so long and complex that it is likely that no single person has ever read them from beginning to end: the classification theorem in group theory is one such - it runs to tens of thousands of pages of work across hundreds of published papers by about a hundred different mathematicians.
When a proof is as difficult as this, it makes sense to enlist the help of automated provers. But it does not completely solve the problem of how to be sure, because we still need assurance that the prover itself is correct. Since the prover is a physical embodiment of a formal proof system, Godel's second incompleteness theorem applies to it: it cannot prove its own consistency. Also, the prover is implemented in hardware and software and we cannot prove there are no errors in the implementation (although formal systems such as Z notation can help).
So to return to your question about Hume, I would say any proof logically conforms to what Hume calls relations of ideas and so is a priori, at least in principle. But there is a hard-headed pragmatic element to Hume's thinking that makes one suspect that he might regard output from a computer as just a kind of empirical evidence. So maybe he would regard a generated proof as a posteriori until it has been internalised and comprehended.
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.
