While there is a boundless, growing amount of prior work, from (an interested) outsiders point of view there also seems to be progress on discoverability and formalisations around how this is expressed. Building on the abstractions of others seems like it would provide an environment for _more_ novel work.

The abstractions need to be understood, but potentially only to a level of n-1. Isn't this one of the core principles of proofs?