Wouldn’t a lot already be in leans mathlib?

A published formalization is code. I would not think humans have any edge when it comes to citing previously published results.

> I am sure a lot of this development was formalising the prerequisites

How can you be so sure its not result of inefficiency?