Privacy and terms

Privacy

This site

The website and proof archive are static pages hosted on Cloudflare; their source files are public on GitHub. This site sets no cookies and loads no advertising or cross-site tracking scripts. Cloudflare processes access logs under its privacy policy.

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

The online workbench is at app.theoremos.top. This section describes how it handles your data.

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 (your first sign-in). We use the address only for sign-in codes and the research-end emails described below, send it no other mail and share it with no one. Mail is delivered by Alibaba Cloud DirectMail from login@mail.theoremos.top.
• Your account also records two times: when you first submitted a run and when a run first passed acceptance. During the preview we use these times to see whether onboarding works, mostly as totals and conversion rates. We 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.

What admins can see

• The workbench admin page lists only: the addresses on the allowlist and where each came from, each account's email address with the times of its first sign-in, first submitted run and first accepted run, and totals built from these times.
• The admin page neither shows nor offers any way to read an account's statements, sources, proofs, run records or API keys. When maintainers look at run records on the server is described under Retention and deletion.

Research-end emails

• When a run ends on its own (finished or failed), the workbench emails your sign-in address with the run title, the outcome, the time taken and a link back to the run. The email contains no statement, source, proof or API key. Runs you stop yourself send nothing.
• This is on by default. Turn off "Email me when research ends" in the account menu to stop it.

Network and hosting

The workbench server is reached through a Cloudflare Tunnel: every request goes over HTTPS to Cloudflare first and is then forwarded to our server. Cloudflare handles this traffic under its privacy policy. To limit code requests, the server counts requests per visitor IP in memory and never writes these counts to disk.

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. By default the browser does not keep it, so you enter it again for each run. If you tick "Remember in this tab", the key is kept in session storage for the current tab, is cleared when you close the tab and is offered only for the same provider and address.

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, your appearance choice (light or dark), 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.