Privacy and terms

Privacy

This site

The website and proof archive are static pages hosted on GitHub Pages. This site sets no cookies and loads no advertising or cross-site tracking scripts. GitHub processes access logs under its privacy statement.

Access requests and feedback

Access requests and feedback sent through GitHub are public issues that anyone can read. Do not include API keys, email addresses or other personal information. Email sent to liuzhenhao@westlake.edu.cn is used only to answer your request and coordinate early access. It is not published or shared.

Online workbench

This section describes how the online workbench handles your data once it opens.

Account and sign-in

• You sign in with a one-time code sent to your email. There is no password. During the preview only approved addresses on the allowlist receive a code.
• The server stores your email address, an account ID and the creation time. We use the address only for sign-in codes, send it no other mail and share it with no one. Code emails are delivered by the mail provider we use.
• Your account also records two times: when you first submitted a run and when a run first passed acceptance. During the preview we look only at totals and conversion rates built from these times, to see whether onboarding works. We do not look at individual accounts and do not record your clicks or page views. Both go when you delete your account.
• Before a code is sent you type a picture captcha. The workbench server draws it; no third-party bot check is used.
• After you sign in, the server sets a session cookie that is sent only over HTTPS and cannot be read by scripts. It keeps you signed in, belongs to the workbench only and is not used for tracking.

API keys

• Your API key is submitted over HTTPS and passed to the isolated container for that run through a private input channel. It does not appear in container arguments or service logs.
• Commands run by the agent do not receive the key in their environment. When a run finishes or is cancelled, the service clears the key from memory and deletes the container.
• If the key appears in model output or an error message, it is replaced with [REDACTED] before anything is saved.
• The key is used only to call the model provider you select in the workbench. The browser never stores it, so you enter it again for each run.

Research records

The server stores the statement, task description and model settings you submit, along with the candidate sources, Lean checks, events and usage produced during the run. These records let you review runs and download archives in the workbench.

Model providers

During a run, the statement, sources and Lean feedback are sent as prompts to the model provider you choose. How the provider handles them is governed by its own privacy policy.

Browser storage

Task drafts, a recovery copy of a replaced draft and panel widths are kept in session storage for the current tab and are cleared when you close it. Local storage holds only your interface language, the desktop notification setting, the run you last viewed (so the workbench reopens where you left off) and module plans you save to the local plan library. None of it contains your API key, and you can clear it in your browser settings.

Feedback from the workbench

"Report a problem" in the workbench opens the feedback page on this site with "Web workbench", your browser, system, window size and interface language filled in, plus the error type after a failed run. It adds no run ID, email address, statement or API key. Opening the page sends nothing; the report is published on GitHub only after you confirm it, and you can edit or remove these details first.

Retention and deletion

• Each account keeps up to 20 run records. You can delete finished runs in the workbench at any time.
• A sign-in expires after 30 days without use. You then sign in again, and your records are kept.
• You can delete your account from the account menu in the workbench. Its email address, run records, archives, knowledge catalogs and server-side module plans are deleted at once, and running tasks are cancelled.
• The maintainers look at run records only to investigate faults or abuse. Your statements and proofs are not used for any other purpose, sold or published.
• Upgrades during the research preview may require clearing data. We will announce this on this site in advance. Download the sources and archives you want to keep.

Terms of use

Research preview

TheoremOS is a research preview provided as is. The service may be interrupted, rate limited or changed. There is no uptime guarantee and no guarantee that a proof will be found.

Costs

The platform is free during the research preview. Model calls are billed to your API key, so set a spending limit with your provider. Usage from runs that fail, are cancelled or time out is billed by the provider as well.

Your content

The statements and sources you submit, and the proofs produced in your runs, remain yours. They appear in the public archive only if you choose to publish them. Submit only content you have the right to use, and do not submit secrets, personal data or confidential material.

Acceptable use

Do not try to break run isolation, attack the service or other users, or upload malicious code, and do not use the run environment for computation unrelated to mathematical research. Sessions that break these rules may be terminated.

Verification results

Verdicts come from an independent Lean check. Review the sources and check records yourself before relying on a result in a paper, competition or other formal setting.

Changes

This page may be updated as the service opens. Significant changes will be dated here and noted on the home page.

Contact

To request deletion of your data or ask about this page, email liuzhenhao@westlake.edu.cn.