4 ms·
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
by owlbite 1mo ago
Interesting, but I don't see any licensing terms, which means I can't touch it in a commercial setting.
- a2ff6eeb0 1mo agoIt's AI generated, so licensing terms are unenforceable.
- a2ff6eeb0 1mo agoOr, 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.
- whattheheckheck 1mo agoIs this effectivly mit or no license?
- a2ff6eeb0 1mo agoEffectively public domain.
- jrflo 1mo agoWhat commercial setting do you want to use a Lean theorem-proving agent in?
- ljwoods2 1mo agoMathematics, Inc [1], I assume [1] http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF http://www.cs.utexas.edu/users/EWD/ewd04xx/EWD427.PDF