Math has Lean. Computational research needs a trace.

On October 6, OpenAI published a GitHub repository of mathematics written by an unreleased internal model: 722 manuscripts in 372 families, drawn from roughly 4,000 problems the model was posed, at an average of three hours of ChatGPT Pro thinking compute per result [1].

The number is striking. What interested us more is how the release asks to be believed.

It ships Lean formalizations for many of the results, and says plainly that not all of them have one yet. It warns that "some of the unformalized results could have issues." It publishes abridged summaries of the model's reasoning for ten results. It promises that corrections will be recorded as new versions, with earlier versions kept public. And it points readers to Comparator, a checker that builds each proof in a sandbox, replays it in Lean's kernel outside that sandbox, and confirms that the theorem proved is exactly the one stated in the challenge. A verified proof of the wrong theorem verifies nothing.

That is the right instinct. When a model can produce research faster than people can referee it, the scarce thing is no longer the result. It is the evidence that the result is right.

Mathematics is in an unusually lucky position here. A Lean proof that compiles has been checked by a small trusted kernel, and it does not matter who, or what, wrote it.

Most of science does not run on proofs. It runs on computation: fitting models to data, simulating physical systems, training networks, testing whether an effect survives a different seed. There is no kernel that certifies a fit. The closest thing computational research has to a proof checker is running the analysis again, and that has never been as easy as it sounds.

Reproduction used to be the expensive part

In 2016, Nature surveyed 1,576 researchers. More than 70% had tried and failed to reproduce another scientist's experiment, and more than half had failed to reproduce one of their own [2].

Computational work should have been the easy case. The machine is deterministic and the code is right there. It was not. In 2019, Pimentel and colleagues tried to run 1.4 million Jupyter notebooks published on GitHub. About 24% ran at all, and about 4% produced the same results they had shown. The leading causes were missing dependencies, hidden state and out-of-order execution, and data that could no longer be reached [3].

So for most computational claims, "reproducible in principle" has meant something closer to "a graduate student, a few weeks, maybe."

What changed

An agent that can read a method, fetch the public data, write the code, run it, look at the figure it made and compare its number with the paper's changes the cost of that sentence.

Over the past month we filmed a series of these on Clusy. Three examples:

• Tirosh et al. (2016) inferred chromosomal copy number from single-cell RNA to tell malignant melanoma cells from normal ones [4]. Starting from the public GEO matrix of 4,645 cells, the session rebuilt the inference and separated the two populations at an AUC of 0.997.
• Mercury's perihelion. An N-body integration of the solar system, forked into two branches, Newtonian and Newtonian plus the first post-Newtonian correction, recovered the relativistic excess as 42.97 arcseconds per century against the textbook 42.98.
• CMS open data. All 61.5 million events in CMS's public 2012 dimuon dataset, streamed in chunks, with six resonance masses fitted to within 0.5% of their Particle Data Group values.

Each ran in one session, from a prompt about the length of a methods section: the data source, the method, a time budget and a numeric self-check that the notebook prints as PASSED or FAILED at the end.

These are known results, with public data and a method we spelled out. That is exactly the reproduction case, and not discovery. But it is the case most of science depends on, and it has quietly gone from weeks to minutes.

When reproduction is cheap, the question changes. It used to be "can anyone rerun this?" Now it is "can anyone see what was actually run?" A generated notebook that prints the right number is not evidence on its own. It is another claim.

A coding agent's idea of done

The same model behaves like a different researcher depending on what it can touch. Eldar wrote about this in Data Science Needs More Than a Coding Agent: change the harness around a fixed model and its results move.

The harness most agents live in today was built for software. Its world is files, a terminal and a test suite. Its unit of work is a diff. Its definition of done is a green test run. And the process that produced the diff is disposable: you squash the commits, and nobody reviews the four approaches that did not compile.

For software, that is correct. Research inverts every part of it.

The unit of work is an experiment on a state: data that took twenty minutes to load, a model trained three cells ago. There is rarely a test that says the answer is right; correctness comes from the evidence and from how it was produced. And the process is not disposable. The variant that lost, the seed that did not hold, the filter that was tried and removed are part of the result. Gelman and Loken called this the garden of forking paths: an analysis can be honest at every step and still mislead, if no one can see how many paths were walked before the one that was reported [5].

A clean final notebook hides exactly that. So does a clean final diff.

Why we built on Jupyter

Jupyter got the hardest part right. A live kernel, with code, output and prose interleaved in one document, is how computational researchers actually think, and the .ipynb file has become the lab notebook of computational science [6].

Its failures are also well documented, and they are the same failures that sink reproductions: hidden state, cells run out of order, outputs that outlive the code that made them, and one linear timeline for work that branches.

A generic coding agent "fixes" this by throwing the kernel away. Everything becomes a script that reruns from the top. That discards the thing that makes notebooks fast for research (state stays loaded; a 2 GB file is read once) and still leaves the history of the work in nobody's hands.

We went the other way. Clusy keeps the kernel, the cells and the notebook you already know, and puts a record around them.

What we changed

The agent works inside the live kernel. It writes a cell, runs it, reads the output back, plots included, and only then decides the next step. Variables persist across cells, so the expensive steps run once, and the Variables tab shows what is in memory at any moment.

Every run is its own record. An execution is stored with its outputs, timing and status, tied to the revision of the cell that ran. Editing the cell afterwards does not erase what it produced before.

Branches fork the state, not the file. When a question has several answers worth trying, the agent forks the notebook from a snapshot of the kernel's memory at that cell, without rerunning the setup above it. Up to eight variants run on their own kernels (three at a time on CPU, eight on GPU). Objects that cannot be serialised, like open file handles, are skipped and named rather than silently lost. Every branch stays in the tree until you or the agent delete it, so the arm that lost is still there to open. Eldar's Data Science as a Search Problem explains why this is the shape research takes.

The agent's reasoning is kept. The reasoning and tool calls of every turn are saved. When a turn finishes they fold under a single row, "Worked for 3m 12s", so the answer stays readable, but the trace is one click away instead of gone.

Plans are a gate, not a suggestion. In plan mode the agent cannot create or run a cell until you approve the plan. That is enforced in the agent's tool layer, not requested in a prompt.

Long runs outlive the browser tab. Cells run on the server and keep running if you close the tab. While the agent works you can send it a correction, and it takes it at its next step.

A session can be handed over whole. A share link carries the notebook and its outputs. If you allow it, a reader can fork it into their own workspace, with its variables if you choose, and start exactly where you stopped.

Python and R cells sit in the same notebook, and a project can run on a CPU or on a T4, A100 or H100 GPU.

The trace is the result

In software, the artifact is the code. In computational research, the artifact is a claim, and the trace is its evidence: what ran, in what order, on what state, what came out, what was tried and dropped, and which check decided it.

That gives us one design rule, and most of the list above follows from it: the clean view never replaces the record. Fold, don't delete. Branch, don't overwrite. Record runs, not just cells.

We have already seen why it matters. In July an agent in Clusy reported a dramatic result: a segmentation model collapsing to zero IoU under a colour shift. We pushed back. It went back through its own runs, found that it had tested the model outside the colour range it was trained on, and withdrew the claim. That was only possible because the runs it went back through were still there.

Back to Lean. A compiling proof is a certificate. A session trace is not one, and it cannot prove an analysis is right. What it can do is make the analysis checkable by anyone willing to rerun it, fork it at the step they doubt, change one thing and compare. For computational research that is the honest analogue of a proof checker: not verified, but verifiable.

What we don't do yet

• No environment lock per run. Package versions and hashes of input data are not recorded with each execution. If a remote dataset changes underneath you, the record says what came out, not which bytes went in.
• Snapshots are not total. Branches carry everything the kernel can serialise; what it cannot is listed, not carried.
• Small scale is small scale. A reproduction that fits in one session shows the mechanism of a result, not always the paper's full number. We will say which, every time.
• Agents are still wrong sometimes. A trace does not prevent that. It makes it findable.

Next: recent papers, in public

Starting this week we are reproducing recent arXiv papers in Clusy, one session per paper, with the whole session shared. When a reproduction fails, we will publish that too. If there is a paper you want to see attempted, send it to us.

Sources

[1] OpenAI, openai/math: mathematical manuscripts and supporting proof artifacts, GitHub, October 2026. github.com/openai/math

[2] M. Baker, "1,500 scientists lift the lid on reproducibility," Nature 533, 452–454 (2016).

[3] J. F. Pimentel, L. Murta, V. Braganholo, J. Freire, "A Large-scale Study about Quality and Reproducibility of Jupyter Notebooks," MSR 2019.

[4] I. Tirosh et al., "Dissecting the multicellular ecosystem of metastatic melanoma by single-cell RNA-seq," Science 352, 189–196 (2016).

[5] A. Gelman, E. Loken, "The garden of forking paths," Columbia University, 2013.

[6] T. Kluyver et al., "Jupyter Notebooks: a publishing format for reproducible computational workflows," ELPUB 2016.