隐私与编辑规则
谁都可以编辑。 本站不需要注册，也不需要 GitHub 账号。每个页面上的编辑按钮都可以直接用。
机器检查，不靠人审。 每条编辑提交后，机器会自动检查格式；新增表述还要编译 Lean，确认没有 sorry、native_decide 或非标准公理，并经 lean4checker 独立复核。检查通过就直接写入，不通过会在状态页说明原因。
不检查等价性。 一条表述是否等价于原猜想，不在检查范围内，也不是编辑或删除的理由。这个问题留给数学家讨论。
我们记录什么。
- 公开记录：你填写的内容、编辑摘要、可选的署名、提交时间，以及一个由你的 IP 地址派生的匿名编号（例如“匿名者 7f3a1c2e”）。同一网络地址在一段时间内编号相同，这样大家能看出哪几条编辑来自同一个人。匿名编号无法反推出 IP。
- 不公开记录：完整的 IP 地址、浏览器标识、大致国家或地区、提交时间。只有维护者能看到，仅用于处理恶意编辑和刷屏，90 天后自动删除。
- 我们不使用 Cookie 追踪你，也不出售或分享任何数据。人机验证由 Cloudflare Turnstile 提供，适用 Cloudflare 的隐私政策。
每条编辑都公开可查。 网站编辑会以“议题”的形式记在 GitHub 仓库里，写入后成为一次提交，页面底部的“编辑历史”列出全部记录。任何编辑都可以被后来的编辑改回来，维护者也可以直接回退。
限制。 每个匿名编号每小时最多提交几次。恶意编辑的网络地址可能被暂停编辑。Lean 代码只允许一个安全的子集：不能使用 #eval、属性标注、元编程、IO 等会在编译时执行代码的写法。
灌水区。 聊天室不需要人机验证。消息和发言者的 IP 一起只保存 7 天；IP 只有维护者可见。每个匿名编号两秒最多一条、每分钟最多三十条。维护者可以删除消息，并暂停刷屏或骚扰者的网络地址 7 天。
许可。 新增表述时由你选择许可，默认 CC-BY-4.0。编辑已有条目，即同意按该条目的许可发布你的修改。改编别人的作品，须沿用原作许可或兼容的许可，并写明原作版权。详见 docs/LICENSING.md。