[kosievdmerwe]

This is why computer based proofs aren't interesting to mathematicians. There is some small amount of value in proving results, but the real value is the new techniques people came up with to prove novel results. As you call it the "high-level abstract algorithm".

Those provide new tools for proving other results and directions for study. A computer based proof will probably just be an incomprehensible mess, think something like an evolved neural net. Not helpful at all.