Terms of use

Short, because the site does little that needs governing. Using Conjectura means agreeing to what follows.

Who is offering this

Conjectura, Inc., in Illinois, United States. These terms are governed by the law of Illinois, United States.

What you may do

Read anything without an account. With one: propose questions, submit proofs, and take part in discussion. The Lean corpus is public and openly licensed; the licence in the repository governs it, not this page.

What you keep

You keep the copyright in what you write and in the proofs you submit. By submitting, you give us permission to store it, check it, and — if you publish it — show it with your name on it. Nothing you keep private is published by us.

What you may not do

• Submit code intended to escape the verifier or reach anything outside it.
• Automate submissions to consume verification capacity others need.
• Post someone else’s work as your own.
• Impersonate a researcher, or claim a maintainer role you were not granted.

The first of those is the one we care about most, and reporting a hole you found is welcomed, not punished.

What a verification does and does not mean

A verified proof means the Lean kernel accepted it against the stated Lean statement, using only the permitted axioms. It does not mean the Lean statement is a faithful rendering of the mathematics. A named maintainer vouches for that separately, and a statement with no maintainer carries no such claim. We publish both facts on every problem so you can tell which you are looking at.

No warranty

The service is provided as it is. Verification is best effort; the sandbox, the toolchain and the site can all have bugs, and a verdict is not a guarantee. To the extent the law allows, we are not liable for losses arising from use of the site.

Ending it

You can stop at any time and ask for your account to be deleted (see Privacy). We may suspend an account that does the things listed above, and we will say which one and why.

Changes

If these terms change materially, everyone with an account gets an email before it takes effect. Silent revision would sit badly on a site whose whole argument is that statements cannot be quietly edited after the fact.