[skybrian]

I don’t share the author’s concern about a corporate takeover of mathematics. Most mathematics isn’t of commercial interest. Even when it is, it seems like there would often good reason to share it, like any other source code. Is Lean so different from other programming languages?

Such libraries would need documentation, or nobody would know when to use them, and then sharing is pointless.

If corporations build them, they would have to decide what to contribute to the commons and what to keep private. But that’s no different than any other language.