Terence Tao on Nostr: nprofile1q…s0ae2 Lean's Mathlib is perhaps in this spirit: . However, it is not ...

nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqd43e6uf946m26zx0r7gddyrxzqtdrplgae776ghc8j2vca2v7uesns0ae2 (nprofile…0ae2) Lean's Mathlib is perhaps in this spirit: https://arxiv.org/abs/1910.09336 . However, it is not aimed towards unrestricted submission; there is a coherent vision for what types of results should be in the library, what format the statements and proofs should be in, and how they should integrate with the rest of the library.