5 ms·

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 correspon

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 4y ago
Creating an extensive library of formally verified results is the goal of many systems, such as http://metamath.org/ http://metamath.org/