|
|
|
|
|
|
by LegionMammal978
447 days ago
|
|
|
The Metamath Proof Explorer (AKA the set.mm database) works on a similar principle, of all theorems forming a tree of backreferences that ultimately lead to the axioms [0]. Though it wouldn't make sense to build something like that on top of such a fast-moving, complex, and bug-prone target like Lean. [0] https://us.metamath.org/mpeuni/mmset.html |
|
|