Comment by owlbite
7 hours ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
7 hours ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
What commercial setting do you want to use a Lean theorem-proving agent in?
Mathematics, Inc [1], I assume
[1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF
It's AI generated, so licensing terms are unenforceable.
Or, more accurately: it's not possible to apply copyright to generated code; if you don't release it, it's a trade secret, but if you do, people can use it how they please.