In research maths, there are some results you use as a black box because even though you could re-derive the result, it’s just a ton of work and you’re glad someone else has done it. For example perhaps it involves some very tedious case-by-case checking, or a large and long inductive argument. Then there are some results you use as a black box because it would take you (in this case you already have a PhD in the field, so let’s say at least 8 years of field-specific education) literally years of full-time study to become familiar enough with the underpinning technology to even follow the statement of the proof, let alone deeply understand it yourself.

I think there are very few, if any, things in software development that have an analogue in that second category.