[HighlandSpring]

And the individual lemmas could have author and chronology metadata attached, then you could plot the DAG as a roadmap/tech tree of sorts with an axis corresponding to time.

You'd be able to at a glance see the year a result entered public domain, who authored it, etc

One can dream

[clcaev]

Creating an extensive library of formally verified results is the goal of many systems, such as http://metamath.org/