Rethlas-OSV: Desktop Math Agents for Mathematicians

Recently, I realized that many mathematicians are interested in trying more advanced AI tools, such as agents, rather than a browser-based chat interface. However, they may not have time for engineering or computer science, and they may not want to spend time working with GitHub and the terminal.

I therefore decided to develop desktop app versions of the mathematical agents I co-developed. They are designed to be easy to install and use through a graphical user interface, for the convenience of mathematicians.

The Rethlas-OSV v0.5.1 beta installers are available here:

• MacBook with Apple silicon (arm64)
• MacBook with an Intel processor (x86_64)

These installers require macOS 12 or later.

This desktop app was mostly vibe-coded with Claude Code Fable 5.1 and built on an early integration of OSVerify and Rethlas by Fan Nie. It is currently in beta, and this release provides installers only for Codex users on macOS. Broader support may be added in the future. We are also continuing to improve OSVerify. Please check this page later for updates.

What Is Rethlas-OSV?

Rethlas-OSV combines Rethlas and OSVerify and runs on OpenAI's Codex. It can generate proofs and report possible imprecisions in a given mathematical paper.

Rethlas is an agentic framework for automated mathematical reasoning, developed by Haocheng Ju, Jiedong Jiang, Shurui Liu, Guoxiong Gao, Yuefeng Wang, Zeming Sun, Leheng Chen, and Bin Wu, under the leadership of Professors Liang Xiao and Bin Dong. Rethlas is fully open source on GitHub. Its technical report also introduces Archon, an agentic framework for autoformalization in Lean 4.

OSVerify is an agentic framework for verification, developed by Fan Nie, Haotian Ye, Shurui Liu, Zihao Wang, Stefano Ermon, and James Zou. The OSVerify paper and code will be released soon.

Why Do I Believe It Is Stronger Than the Base Model Alone?

There is no theoretical proof or guarantee that this harness improves the capabilities of the base model, but quite a few case studies suggest that it does. Some are included in the Rethlas technical report and the forthcoming OSVerify paper. Several users have also observed improvements over using the base model alone with GPT-5.5 Pro, GPT-5.6 Sol, and GPT-6-Astra.

How to Use It

Installation

1. Download the app for your Mac: Apple silicon (arm64) or Intel (x86_64). To identify your processor, open the Apple menu in the upper-left corner of your screen and select About This Mac.
2. Double-click the disk image and drag Rethlas-OSV into Applications. If macOS offers to move the app to the Trash, do not select Move to Trash.
3. On the first launch, you need to grant permission. Double-click the app once and dismiss the warning by selecting Done. Then open System Settings, select Privacy & Security, scroll down, and click Open Anyway next to the Rethlas-OSV message.

From then on, you can use it like any other app on your MacBook. Press command+space and type reth to open it quickly.

Sign In to Your Codex Account

Open Settings and click Sign in.... Rethlas-OSV will open your browser and ask you to sign in to the OpenAI account you use with Codex.

Find Mistakes in a Paper

You can use Rethlas-OSV to find mistakes in a paper. Load the paper's LaTeX source or Markdown file, and give the run a name.

Then choose a mode. The default is Smart mode, in which the agent selects the main theorems and the key steps on which they depend.

Next, decide whether you want to enable Stop on audited rejection. When this option is enabled, the review stops early if it produces an audited REJECT decision. When it is disabled, the agent completes the entire process and reports all the issues it finds.

After choosing the model and reasoning effort, click Start review.

Prove a Conjecture or a Lemma

Give the project a run name. You can then enter the problem, for example:

• Prove Conjecture 4.16 in arXiv:xxxx.xxxx.
• Prove or disprove the conjecture that ...
• Load the LaTeX file for your ongoing work and add Prove the lemma {LaTeX tag} in the following paper at the beginning.

Then choose the model, reasoning effort, maximum number of rounds per branch (how many iterations it will try), and number of parallel branches (how many generation agents should work on different strategies in parallel).

Click Start proving to begin.

Manage Runs

You can cancel a run and resume it later. If you run out of GPT quota or need to shut down your laptop, do not worry: your completed work is retained, and you can resume later.

Suggestions for Users

1. Rethlas-OSV requires a GPT subscription. Its settings and every run's inputs, reports, and execution records remain on your computer; the desktop app stores them in ~/Library/Application Support/Rethlas-OSV/. Model calls go to OpenAI through the Codex CLI under your own account. Rethlas-OSV stores no credentials, and apart from model calls to OpenAI through Codex, it sends no data elsewhere.
2. Please use Rethlas-OSV responsibly. People may hold different philosophical views about the future of mathematics and its protocols, but please make sure that you intend to benefit the mathematical community and humanity.
3. Monitor the usage on your GPT account. An agentic workflow may be expensive because it calls the base model continuously.
4. If you use Rethlas-OSV to generate proofs, make sure that you assign credit appropriately. A generated solution may not properly attribute previous work or ongoing work in the mathematical community.
5. If you use Rethlas-OSV to review papers, make sure that you obtain permission from the authors, the journal, and any other parties involved. Rethlas-OSV reports only detected correctness issues and makes no judgment about a paper's novelty or significance.
6. Like any AI tool in mathematics, Rethlas-OSV does not guarantee correctness.
7. Please be transparent about your use of generative AI. Use common sense and your own judgment.
8. We would deeply appreciate it if you cited our papers.

References

[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},
}

A More Detailed Demo

A more detailed demo will be added here.

Acknowledgements

I sincerely thank all my collaborators on Rethlas and OSVerify. In particular, I want to thank Bin Dong, Guoxiong Gao, Haocheng Ju, Fan Nie, and Haotian Ye for their support and for the wonderful experience of working together.

I also want to thank members of the Stanford mathematics community for their constant support. In particular, I want to thank Kevin Rizk and Henry Bosch for testing the desktop app before I made it public.