Add a license

[MithicSpirit]

Since the project currently does not contain any form of license, people are technically disallowed from using it in any way (except where covered by laws such as fair use). I believe that this is not intended, considering there are instructions in the README on using this project. Popular options for permissive licenses are Apache (used by Lean itself and Mathlib) and MIT (relatively simple and brief), among others. For the most part, adding a license only requires creating a LICENSE file with the contents of the desired license, though it may also be desirable to add a note to the README or add headers to the files indicating the license. It is also necessary to make sure all contributors agree with this, as they likely retained their copyright on their code.

I am not a lawyer; this is not legal advice.