刘抒睿

Rethlas-OSV：为数学家打造的桌面数学智能体

刘抒睿

最近，我意识到，许多数学家有兴趣尝试比浏览器聊天界面更先进的 AI 工具，例如智能体。然而，他们可能没有时间钻研工程或计算机科学，也可能不想花时间折腾 GitHub 和终端。

因此，我决定为自己参与开发的数学智能体制作桌面应用版本。这些应用旨在通过易于安装和使用的图形用户界面，为数学家提供便利。

Rethlas-OSV v0.5.1 测试版安装程序可在此下载：

这些安装程序需要 macOS 12 或更高版本。

这款桌面应用主要使用 Claude Code Fable 5.1 进行 vibe coding，并以 Fan Nie 早期完成的一版 OSVerify 与 Rethlas 集成为基础。目前它仍处于测试阶段，本次发布仅向在 macOS 上使用 Codex 的用户提供安装程序。将来如有需要，我们可能会扩大支持范围。我们也在继续改进 OSVerify。请稍后再查看本页面以获取更新。

什么是 Rethlas-OSV？

Rethlas-OSV 将 Rethlas 与 OSVerify 结合起来，运行于 OpenAI 的 Codex 之上。它可以生成证明，也可以指出某篇数学论文中可能存在的不严谨之处。

Rethlas 是一个用于自动数学推理的智能体框架，由 Haocheng Ju、Jiedong Jiang、Shurui Liu、Guoxiong Gao、Yuefeng Wang、Zeming Sun、Leheng Chen 和 Bin Wu 开发，并由 Liang Xiao 教授和 Bin Dong 教授领导。Rethlas 已在 GitHub 上完全开源。其技术报告还介绍了 Archon——一个用于 Lean 4 自动形式化的智能体框架。

OSVerify 是一个用于验证的智能体框架，由 Fan Nie、Haotian Ye、Shurui Liu、Zihao Wang、Stefano Ermon 和 James Zou 开发。OSVerify 的论文和代码将很快发布。

为什么我认为它比单独使用基础模型更强？

目前并没有理论证明可以说明这一框架能提升基础模型的能力，也没有任何这方面的保证；不过，已有相当多的案例研究表明，它确实能做到这一点。其中一些案例收录在 Rethlas 的技术报告和即将发布的 OSVerify 论文中。多位用户也观察到，将这一框架与 GPT-5.5 Pro、GPT-5.6 Sol 和 GPT-6-Astra 搭配使用，效果比单独使用这些基础模型更好。

如何使用

安装

  1. 下载适用于你的 Mac 的应用：Apple 芯片（arm64）或 Intel（x86_64）。要确认处理器类型，请打开屏幕左上角的苹果菜单，然后选择 About This Mac（关于本机）。
  2. 双击磁盘映像，然后将 Rethlas-OSV 拖入 Applications（应用程序）。如果 macOS 提示将应用移到废纸篓，请不要选择 Move to Trash（移到废纸篓）。
  3. 首次启动时，你需要授予权限。先双击应用一次，然后选择 Done（完成） 关闭警告。接着打开 System Settings（系统设置），选择 Privacy & Security（隐私与安全性），向下滚动，并在 Rethlas-OSV 提示旁点击 Open Anyway（仍要打开）。

从此以后，你就可以像使用 MacBook 上的其他应用一样使用它。按下 command+space 并输入 reth，即可快速打开它。

登录你的 Codex 账户

打开 Settings，然后点击 Sign in...。Rethlas-OSV 会打开浏览器，并要求你登录用于 Codex 的 OpenAI 账户。

Rethlas-OSV 中的 Codex CLI 登录设置

找出论文中的错误

你可以使用 Rethlas-OSV 找出论文中的错误。加载论文的 LaTeX 源文件或 Markdown 文件，并为本次运行命名。

在 Rethlas-OSV 中加载论文并选择验证模式

然后选择一种模式。默认模式是 Smart；在这种模式下，智能体会选择主要定理，以及这些定理所依赖的关键步骤。

Rethlas-OSV 中的验证选项和 Start review 按钮

接下来，决定是否启用 Stop on audited rejection。启用此选项后，如果审查流程给出经过审计的 REJECT 判定，就会提前停止。禁用此选项后，智能体会完成整个流程，并报告它发现的所有问题。

选择模型和推理强度后，点击 Start review。

证明一个猜想或引理

为这个项目指定一个运行名称。然后，你可以输入问题，例如：

  • Prove Conjecture 4.16 in arXiv:xxxx.xxxx.
  • Prove or disprove the conjecture that ...
  • 加载你正在进行的工作所对应的 LaTeX 文件，并在开头添加 Prove the lemma {LaTeX tag} in the following paper。
在 Rethlas-OSV 中配置一次证明生成任务

然后选择模型、推理强度、每个分支的最大轮数（即它会尝试多少次迭代），以及并行分支数（即有多少个生成智能体应当并行探索不同的策略）。

点击 Start proving 即可开始。

管理运行任务

你可以取消某次运行，并在之后恢复它。如果 GPT 配额用尽，或者需要关闭笔记本电脑，也不必担心：已经完成的工作会得到保留，你可以稍后恢复运行。

给用户的建议

  1. Rethlas-OSV 需要 GPT 订阅。它的设置以及每次运行的输入、报告和执行记录都会保留在你的电脑上；桌面应用会将它们存储在 ~/Library/Application Support/Rethlas-OSV/ 中。模型调用会通过 Codex CLI，并使用你自己的账户发送到 OpenAI。Rethlas-OSV 不存储任何凭据；除了通过 Codex 向 OpenAI 发出的模型调用外，它不会向其他任何地方发送数据。
  2. 请负责任地使用 Rethlas-OSV。人们对于数学及其规范的未来，可能持有不同的哲学观点，但请至少确保你的本意是造福数学界和人类。
  3. 请留意 GPT 账户的使用量。智能体工作流会持续调用基础模型，因此费用可能很高。
  4. 如果你使用 Rethlas-OSV 生成证明，请务必妥善注明贡献归属。生成的解答可能无法恰当地注明既有工作或数学界正在进行的工作所作的贡献。
  5. 如果你使用 Rethlas-OSV 审查论文，请确保已获得作者、期刊和其他所有相关方的许可。Rethlas-OSV 只报告检测到的正确性问题，不对论文的新颖性或重要性作出判断。
  6. 与任何数学 AI 工具一样，Rethlas-OSV 不保证正确性。
  7. 请透明地说明你对生成式 AI 的使用。请运用常识和你自己的判断。
  8. 如果你能引用我们的论文，我们将不胜感激。

参考文献

[1] Haocheng Ju, Guoxiong Gao, Jiedong Jiang, Bin Wu, Zeming Sun, Shurui Liu, Leheng Chen, Yutong Wang, Yuefeng Wang, Zichen Wang, Wanyi He, Peihao Wu, Liang Xiao, Ruochuan Liu, Bryan Dai, and Bin Dong. Automated Conjecture Resolution with Formal Verification. arXiv:2604.03789, 2026.

[2] Fan Nie, Haotian Ye, Shurui Liu, Zihao Wang, Stefano Ermon, and James Zou. One-Sided Verification Under Limited Expert Review. In submission, 2026.

BibTeX

@misc{rethlas_archon2026,
  title  = {Automated Conjecture Resolution with Formal Verification},
  author = {Haocheng Ju and Guoxiong Gao and Jiedong Jiang and Bin Wu and
            Zeming Sun and Shurui Liu and Leheng Chen and Yutong Wang and
            Yuefeng Wang and Zichen Wang and Wanyi He and Peihao Wu and
            Liang Xiao and Ruochuan Liu and Bryan Dai and Bin Dong},
  note   = {arXiv:2604.03789},
  year   = {2026},
}

@misc{osv2026,
  title  = {One-Sided Verification Under Limited Expert Review},
  author = {Fan Nie and Haotian Ye and Shurui Liu and Zihao Wang and
            Stefano Ermon and James Zou},
  note   = {In submission},
  year   = {2026},
}

更详细的演示

更详细的演示将添加在这里。

致谢

我衷心感谢所有 Rethlas 和 OSVerify 的合作者。特别是，我要感谢 Bin Dong、Guoxiong Gao、Haocheng Ju、Fan Nie 和 Haotian Ye 给予我的支持，以及与他们合作的这段美好经历。

我也要感谢斯坦福数学界的朋友们一直以来的支持。特别是，我要感谢 Kevin Rizk 和 Henry Bosch 在这款桌面应用公开发布前对它进行测试。

Comments