Math agent researchers
Keep the problem, model and budget fixed, then swap the search, context or collaboration strategy to see which works better. Every attempt keeps its candidates, diagnostics and usage.
TheoremOS
A research runtime for math agents.
Connect your model. Verify Lean proofs independently.
Explore in chat,
verify in the workspace.
The research chat and the Lean workspace sit side by side. On phones and tablets you can switch views to see the statement, the source and the check status.
Who it serves,
and what it costs.
Submit a Lean statement and choose a model and budget. TheoremOS runs the research and the independent check.
Lean and Mathlib users
Hand a theorem with sorry to a model. A result counts only when the full statement passes an independent Lean check, and you can download the source and the report.
Cost
The platform is free during the research preview. Model calls use your own API key and are billed at your provider's prices. Set turn and time limits before you submit. A run lasts at most 15 minutes.
How API keys are handledFrom candidate
to verification.
A four-step replay of a recorded proof. The source, checks and repair are kept together with the final receipt.
See the full replay recordtheoremos / local-replayPreset replay · no model calls
Submission.leanPreset candidate 01
namespace Tutorialtheorem add_zero (n : Nat) : n + 0 = n := by rfltheorem zero_add (n : Nat) : 0 + n = n := by rflend TutorialLean feedbackWhat the check found
What the check found in the preset candidateOne goal passes,
One goal passes,
one needs more work.
add_zero closes with rfl;zero_add needs an existing lemma.
n : Nat
⊢ 0 + n = nThe next candidate uses Nat.zero_add n.
Submission.leanPreset candidate 02
namespace Tutorialtheorem add_zero (n : Nat) : n + 0 = n := by rfltheorem zero_add (n : Nat) : 0 + n = n := by exact Nat.zero_add nend TutorialSubmission.leanVerified source
namespace Tutorialtheorem add_zero (n : Nat) : n + 0 = n := by rfltheorem zero_add (n : Nat) : 0 + n = n := by exact Nat.zero_add nend TutorialPreset example · archived final receipt · not a live runReplay record
Results you
can check.
| Problem and original research record | Area | Verification and evidence |
|---|---|---|
DimitrovA lower bound for the house of algebraic integers DeepScientist Math + GPT-6.1 (gpt-6.1-sol) |
Number theory | Official pass |
Hopf–RinowGeodesic and metric completeness DeepScientist Math + GPT-6.1 (gpt-6.1-sol) |
Riemannian geometry | Official pass |
Fractional expectation thresholdsThreshold bounds for up-closed families DeepScientist Math + GPT-6.1 (gpt-6.1-sol) |
Probabilistic combinatorics | Official pass |
Equiangular linesEquiangular lines with a fixed angle DeepScientist Math + GPT-6.1 (gpt-6.1-sol) |
Discrete geometry | Official pass |
Rademacher & Enflo typeRademacher type and Enflo type coincide DeepScientist Math + GPT-6.1 (gpt-6.1-sol) |
Functional analysis | Official pass |
Unit conjectureA nontrivial unit in a group ring DeepScientist + GPT-5.6 |
Algebra | Official pass |
These results come from the predecessors DeepScientist and DeepScientist Math and from later work, including resumed runs and environment migrations. Each archive record lists the original attribution, the official result and the source.
Five decisions,
studied in combination.
Fix the statement, environment, model and budget, then swap one kind of research decision. Five research components support single-agent and multi-agent comparisons.
Give the next step a rule.
Picks ready tasks and decides whether to continue, retry or stop. Study task ordering together with route and budget constraints.
- Input
- Research state · candidate operations · shared budget
- Output
- Next operation · ordered ready tasks
M3 · Search
An independent Lean pipeline always verifies the full original statement.
See the research
as it happens.
From the statement and model settings to the final archive, every screenshot comes from the running product. The interface is currently in Chinese.
Open the proof archive
Statement and source, side by side.
Pick the Lean standard library or a fixed Mathlib environment, then check candidates and diagnostics in the workspace on the right. This screenshot shows an unsubmitted draft.
Web workbench
Download the Lean source and the verification report. Sign in with an email code; run records belong to your account.
Request accessResearch record
Candidates, diagnostics and total usage are saved, so you can review a study afterwards.
Browse the proof archive
Connect your own model.
Works with OpenAI and services compatible with the Responses API. Your API key is never written to browser storage.
Start your
next study.
The online workbench is coming soon.
Request access and we will reply in the same issue when it opens.
GitHub requests are public. Do not include API keys, email addresses or other personal information. Without GitHub, or to apply privately, email liuzhenhao@westlake.edu.cn.
Online workbench
Coming soon
- Submit Lean and Mathlib statements, then follow the research chat and workspace online
- Use your own API key; it is never written to browser storage
- Download the Lean source and the verification report
A full statement passes only with
evaluated_passedBefore you start.
How do I request access?
Open an early access request on GitHub and describe your research use and the problems you want to work on. We will reply in the same issue when the workbench opens and ask you to email us the address you will sign in with. Once it is on the allowlist, you sign in with a code sent to that address. Requests are public, so do not include API keys, email addresses or other personal information. Without GitHub, or to apply privately, email liuzhenhao@westlake.edu.cn with your research use and the problems you want to work on.
What is it for?
It is built for math agent researchers and Lean developers: building proofs, comparing search and collaboration methods, and reviewing research experiments. This is a research preview.
Can I run proofs in the browser?
The online workbench is coming soon. Once it opens, you can submit Lean and Mathlib statements in the browser, enter your own API key and see the verification result. For now the site offers interface screenshots, a recorded replay and the proof archive.
Which API keys are supported?
The online workbench works with OpenAI and services compatible with the Responses API. Research runs incur usage with your provider. The recorded replay on this site does not call a model and needs no API key.
Does the web workbench keep my research records?
Run records are stored on the server under your account, and you can download the source and reports. All records are deleted when you delete your account. Your API key exists only in memory during a run and is never written to disk or browser storage. See Privacy and terms.