Terms of Service
Plain terms for a small site. Use it in good faith and none of this will matter.
1. Your account
An account is a username and a password. An email address is optional and used only to reset a forgotten password — without one, a forgotten password means the account is gone, and we cannot recover it for you. You are responsible for what happens under your account. One person, one account; do not use extra accounts to vote on your own posts.
2. What you post
You keep ownership of what you write. By posting you grant us a non-exclusive licence to display it here and in the site's feeds and archives. Posts and their verification receipts are public.
3. Code execution
Code in a fenced block runs on our servers in an isolated sandbox. You may not use it to attack the sandbox or anything else, mine cryptocurrency, store or serve unrelated data, or work around the compute allowance. We may stop any run, refuse further runs, or close an account for doing so.
4. Compute and credit
Every account gets a monthly allowance of tool time at no charge. Beyond it you may buy prepaid credit, which is spent at the rate shown on the pricing page. Credit does not expire and is not transferable. Running out of compute never destroys your work: the run is kept and retried when you have allowance again.
5. Refunds
If a run fails because of a fault on our side, the compute is not charged. For anything else, ask — unused credit is refundable within 30 days of purchase.
6. What the mark means, and does not
∎ means the Lean kernel accepted a submitted proof against Mathlib
with no sorry, no new axiom and no skipped type-checking. That is
a strong statement about the Lean file and a weaker one about the world: it
does not certify that the formal statement says what its author claims in
English. Nothing here is a warranty of mathematical correctness, and results
from this site are provided as-is.
7. Conduct
No harassment, no spam, no deliberately misleading claims about what a run showed. We can remove content and close accounts at our discretion.
8. Availability
The service is provided without warranty of availability. Checkers go down; when they do the site says so on the status page rather than reporting a failed proof.
9. Liability
To the extent permitted by law, our liability for any claim relating to this service is limited to the amount you paid us in the twelve months before it arose.
10. Changes
We may update these terms; material changes will be announced on the site. Continuing to use it after that means you accept the revised terms.