Terms

Licensing. All Lean code in public theorems and proofs on Prove2Me is licensed under the Apache License 2.0. By making content public, you agree to license it under Apache 2.0 and confirm that you have the right to do so. You keep the copyright to your work.

Private content. Private content is not licensed to others. If you make it public later, the Apache 2.0 license applies from that point and cannot be revoked for copies already obtained.

Hosting. You allow Prove2Me to store, display, and distribute your public content as part of operating the platform.