Infrastructure for Math 2.0
The operating system for collaborative
math research and scientific computing.
Built on open frontier models, with the mathematical community in control of its data.
Is 1 + 3 + ⋯ + (2n − 1) always a perfect square? Check it, prove it in Lean, and add it to the paper.
- Pythonexploration.pyChecked n ≤ 10,000 — always n²
- LeanOddNumbers.leanProved by induction · no goals
- LaTeXpaper.texAdded Proposition 2.1 with proof
Yes—the first n odd numbers sum to n². The Lean proof and the write-up are ready for your review.
The platform
Models, compute, data, and people—in one system.
Open frontier models
Leading open-source models, with agents exploring problems in parallel.
02Scientific compute cloud
A 24/7 cloud machine for every project, with 100+ mathematical and scientific computing tools preinstalled.
03Data sovereignty
The mathematical community owns its data and decides how it is used.
04Collaboration tools
People and AI agents, united through shared projects, files, and conversations.
01Open frontier models
Frontier reasoning, built in the open.
Choose the most capable open-source models and set the reasoning depth for each research task. Open weights let the community inspect, improve, and run them.
Model
- Kimi K3Open weights
- DeepSeek V4.1 FlashOpen weights
- GLM 5.3 FlashOpen weights
- Open Math ModelComing
Ultramath
Explore in parallel. Bring the findings together.
Ultramath is Ultracode for math: agents pursue different approaches to one problem, share findings, and return proposed solutions to your chat. You decide what holds.
Reports
02Scientific compute cloud
A mathematical laboratory for every project.
Every project has its own cloud machine with 100+ preinstalled tools for mathematics and scientific computing. Work runs 24/7, even with your laptop closed. Your files and results are there when you return.
- Work in your browser. No local setup.
- Upload files and folders. Download results into your workflow.
- Browse, preview, and edit files alongside the conversation.
Symbolic computation
from sympy import symbols, summation
k, n = symbols("k n", integer=True, positive=True)
summation(2*k - 1, (k, 1, n))theorem sum_odd (n : ℕ) :
∑ i ∈ Finset.range n, (2 * i + 1) = n ^ 2 := by
induction n with
| zero => simp
| succ k ih => rw [Finset.sum_range_succ, ih]; ring03Data sovereignty
The mathematical community, in control.
Open Math OS upholds a core Open Math Model principle: the mathematical community owns its data and decides how it is used.
Private by default
Your team’s projects, files, and chats stay private until you choose to share them.
Consent before training
Training on your work requires your explicit consent, on terms agreed in advance.
Rules set in public
The community governs data collection and use.
Credit stays with you
You retain ownership of your work and credit for your ideas.
04Collaboration tools
Mathematicians and AI agents.
One research team.
Divide the work, from proving lemmas to revising the paper. People and agents share the same projects, files, and conversations.
- Share chats by link, with their history, so colleagues can follow the reasoning.
- Keep projects focused. Bring materials together when a task spans multiple projects.
Find a proof of this lemma.
I’ve added the proof to proof.lean for your review.
Move Section 3.1 to Section 4 in the paper draft.