Terms of use
qed.bot is run by its operator ("we"). These terms cover your use of qed.bot, including accounts, discussion, bounties and games. Creating an account means you accept them. How we handle personal data is set out in the privacy policy.
The register
The register records what has been claimed about artificial intelligence and mathematics, what evidence is attached, and what has been checked. Its grades describe that evidence; they are not a verdict on the mathematics. It is assembled from public sources, which are cited, and it can be wrong. Corrections are welcome on the corrections page, or at hello@qed.bot. Do not rely on it as the only basis for a decision that matters to you.
The register's datasets are published under the Creative Commons Attribution 4.0 licence: you may copy, adapt and build on them for any purpose, crediting qed.bot. Each record cites its sources, and data drawn from other registries keeps its own licence.
Accounts
Accounts are free and for people aged 16 and over. Keep one account, give accurate information, and keep your ways of signing in secure: you are responsible for what is done from your account.
Community rules
Keep discussion about the mathematics and the evidence. Do not:
- harass, threaten or abuse anyone, or post hateful content;
- post anyone's personal information, or anything unlawful;
- impersonate anyone, or misrepresent who did a piece of work;
- spam, advertise, or post malicious links or code;
- manipulate votes, whether with several accounts or by coordinating with others;
- post work that is not yours to share.
Votes express readers' opinions and never change a grade. Anyone can report a post or reply, and we may hide content, remove it, or suspend accounts that break these rules.
What you post
You keep ownership of what you post. You give us a worldwide, non-exclusive, royalty-free licence to host, display and link to it on qed.bot. When you delete your account, your posts and replies stay, attributed to a deleted account, so that discussions remain readable.
Corrections, results and claims
Anyone with an account can ask for a correction to a record, report a result the register should hold, or add a claim of AI work to a record. Each must cite its sources, and is public from the moment it is sent, under your handle, with a discussion thread. A Lean proof attached to a claim is checked as bounty proofs are, and the outcome of each check is shown with it. An administrator accepts or declines each item in public, giving the reason for a decline. An accepted claim enters the register at its next refresh, graded by the register's rubric from what was checked and from its sources; other accepted items are applied to the register by hand, in the register's own words. By adding a claim you agree that, once accepted, it is published in the register's datasets under their licence, with your handle as the reader who added it.
Add only claims your sources support, and name the systems and people who did the work as your sources name them. Sending one does not oblige us to change the register, and votes and replies never change a grade. We may hide a correction, report or claim that breaks the community rules.
Claiming a claim
If a claim in the register is your work, you can say so. You are recorded as an author when the GitHub account you connected owns, contributes to, or publicly belongs to the organisation behind a repository the claim cites that holds only that work, or when an administrator verifies you from the evidence you give; the page says which. As an author you can post a statement shown beside the claim, and ask for its grades to be reviewed. Being recorded as an author never changes a grade.
Claim only work you did, and give only evidence that is true. We may remove an authorship, or a statement, that is false or breaks the community rules.
Bounties
A bounty is a pledge from one person to whoever first proves a statement to qed.bot's standard. A claim passes two checks. First, qed.bot's checker builds the proof at the commit submitted and confirms that it rests on the standard axioms alone. Second, the proof must prove the statement as the register records it: where the claim imports the register's formal statement and names its theorem, the Lean kernel checks that the two statements are exactly the same; otherwise an administrator confirms it. The outcome of each check is shown with the claim.
- A bounty is published only after its pledger enters a code sent to the email address they give, confirming that the address works. The name the pledger gives is shown with the bounty, together with their handle; the address is not shown.
- The terms shown with a bounty are the terms it was published under, and they do not change afterwards.
- So that nothing in a proof can alter what the checks report, a bounty proof's project configures Lake with
lakefile.toml, takes every package from its official repository, and defines no syntax, notation or metaprograms, even in comments. A claim that breaks these rules is refused before anything in it is run. - The pledger alone is responsible for paying. qed.bot holds, moves and guarantees no money, and is not a party to any agreement between a pledger and a claimant.
- The checks record whether a proof meets that standard. They are not a legal determination, and any dispute about payment is for the pledger and claimant to settle.
- Pledge only what you intend to pay, and only under your own name or one you are entitled to use. We may remove bounties or claims that look fraudulent or unlawful.
Games
The games are for enjoyment. They carry no prizes, and scores and leaderboards may be reset.
The service
qed.bot is provided as it is. We may change, pause or end any part of it, and we do not promise that it will always be available or free of errors.
Liability
As far as the law allows, we are not liable for indirect or consequential loss, or for loss arising from reliance on the register. Nothing in these terms limits liability for fraud or for anything else that the law does not allow to be limited, and nothing affects the rights the law where you live guarantees you as a consumer.
Ending
You can delete your account at any time from your account page. We may suspend or close an account that breaks these terms.
Law
These terms are governed by the laws of the State of Delaware, without regard to its rules on conflicts of law, and disputes belong to the state and federal courts in Delaware. If you live elsewhere, you keep any protection the law where you live gives you that an agreement cannot take away.
Changes and contact
When these terms change, the date at the top changes with it, and significant changes are announced to account holders by email before they take effect. Write to hello@qed.bot with any question.