隐私与条款

隐私说明

本站

官网和证明档案是托管在 GitHub Pages 上的静态页面。本站不设置 Cookie，不加载广告或跨站追踪脚本。GitHub 会按其隐私声明处理访问日志。

内测申请与反馈

通过 GitHub 提交的内测申请和反馈是公开 Issue，任何人都能看到。请不要在其中填写 API Key、邮箱等个人信息。发送到 liuzhenhao@westlake.edu.cn 的邮件只用于回复申请和沟通内测，不会公开或转给他人。

在线工作台

以下内容说明在线工作台开放后如何处理你的数据。

账号与登录

• 工作台用邮箱验证码登录，没有密码。内测期间只有通过申请、加入白名单的邮箱能收到验证码。
• 服务器保存你的邮箱、账号 ID 和创建时间，只用于登录和发送验证码，不发送其他邮件，也不提供给他人。验证码邮件经我们使用的发信服务商投递。
• 账号还记录两个时间：第一次提交运行和第一次通过验收。内测期间我们只看这些时间汇总成的人数和转化率，用来判断引导是否有效，不看单个账号，也不记录你的点击或浏览。删除账号时一起删除。
• 发送验证码前需要输入图形验证码。图形验证码由工作台服务器生成，不使用第三方人机验证服务。
• 登录后，服务器设置一个仅限 HTTPS 传输、脚本无法读取的会话 Cookie，用来保持登录。这个 Cookie 只属于工作台，不用于追踪。

API Key

• API Key 通过 HTTPS 提交，经私有输入通道传入本次运行的隔离容器，不出现在容器启动参数或服务日志中。
• Agent 执行命令时，环境变量中不含 API Key。运行结束或取消时，服务清除内存中的 Key，并删除容器。
• 如果模型输出或错误信息中出现了 Key，保存前会替换为 [REDACTED]。
• Key 只用于调用你在工作台中选择的模型服务。浏览器不会把 Key 写入本地存储，每次运行需要重新输入。

研究记录

服务器保存你提交的原题、任务说明和模型配置，以及运行中产生的候选源码、Lean 检查结果、事件和用量。这些记录用于在工作台中回看运行和下载档案。

模型服务商

运行时，原题、源码和 Lean 反馈会作为提示发送给你选择的模型服务商。服务商如何处理这些内容，以其自身的隐私政策为准。

浏览器存储

任务草稿、被替换草稿的恢复副本和面板宽度保存在当前标签页的会话存储中，关闭标签页即清除。浏览器本地存储只保存：界面语言、桌面通知开关、上次查看的运行（用于下次打开时回到原处），以及你保存到"本机方案库"的模块方案。这些都不含 API Key，可以在浏览器设置中清除。

工作台里的反馈入口

工作台的"反馈问题"会打开本站的反馈页，并预先填好"网页工作台"、浏览器、系统、窗口尺寸和界面语言；运行出错时还会附上错误类型。不包含运行 ID、邮箱、原题或 API Key。打开反馈页不会发送任何内容，你确认后才会在 GitHub 公开发布，发布前可以修改或删掉这些信息。

保存与删除

• 每个账号最多保存 20 条运行记录。已结束的运行可以在工作台中随时删除。
• 登录 30 天未使用即过期，需要重新登录，记录保留。
• 在工作台的账号菜单中可以删除账号。删除后，账号的邮箱、运行记录、档案、知识目录和服务器上的模块方案立即全部删除，运行中的任务会被取消。
• 维护者只在排查故障或处理滥用时查看运行记录，不会把你的原题或证明用于其他目的，也不会出售或公开。
• 研究预览期间，服务升级可能需要清空数据，届时会提前在本站说明。请及时下载需要保留的源码和档案。

使用条款

研究预览

TheoremOS 目前是研究预览版本，按现状提供。服务可能中断、限流或调整功能，不保证可用时间，也不保证一定能得到证明。

费用

研究预览期间平台不收费。模型调用由你的 API Key 计费，请在服务商处设置额度上限。运行失败、取消或超时，已产生的模型用量同样由服务商计费。

你的内容

你提交的原题、源码和运行中得到的证明仍归你所有。只有你选择公开发布时，它们才会出现在公开档案中。请只提交你有权使用的内容，不要提交密钥、个人数据或保密材料。

合理使用

不得尝试突破运行隔离、攻击服务或其他用户、上传恶意代码，也不得把运行环境用于与数学研究无关的计算。违反这些规定的会话可能被终止。

验收结果

验收结论来自独立的 Lean 检查流程。用于论文、竞赛或其他正式场合前，请自行复核源码和检查记录。

变更

本页内容可能随服务开放而更新。重大变更会在本页标明日期并在首页提示。

联系方式

需要删除数据或对本页有疑问，请发邮件至 liuzhenhao@westlake.edu.cn。