How we work

Each project is a problem that one of our researchers has chosen to work on. AI agents propose far more questions than we take up, and we start on one only when someone thinks it is worth several weeks of work. Before the work begins, we write down what would count as an answer and which assumptions and methods are allowed.

The work happens in the project’s own space in Mantis. Agents there search the literature and the project’s earlier attempts. They also write and run code and draft arguments, which the researchers read and revise. Everything is saved as a record that points to the file and lines it came from, so any claim can be traced back to its source.

Before a claim goes into a paper, someone who did not write the argument reads it in full, and an audit compares the claim with the records behind it. When the audit finds a mistake, the draft is corrected and the record of the mistake stays in the space.

When a proof comes down to a finite set of cases, a program checks every case and saves its output as a certificate. Each certificate has a negative control, an altered input that the checker has to reject. Our opaque sets paper, for example, checks its inequalities in exact arithmetic for all 105 six-leaf topologies and all 45 five/four-leaf pairs.

Every abstract says what the result does not cover. The gyrokinetics paper reports that ordinary orbit averaging changes the stationary field by 23.2%, and states that the figure is stable under its grid refinements but is not a certified continuum value.

Our clique minors paper proves bounds for H, the complement of the Higman-Sims graph. The project notes list six open questions about H. The first asks whether had(G) ≥ χ(G) for every inflation G of H, and the paper grew out of it (Figure 1a).

An early draft claimed had(H[S]) ≥ χ(H[S]) − 8 for every induced subgraph H[S] (Figure 1b). The audit of that draft found that the proof used χ(G) ≥ ⌈n/2⌉, which holds for graphs with α(G) ≤ 2, as if it were an upper bound on χ(G) (Figure 1c).

The argument was rebuilt. The first rewrite gave an explicit K₅₆ model in H and proved had(H[S]) ≥ χ(H[S]) − 6. A later revision replaced its separation argument with a construction that works for every graph with independence number at most two, which improves the bound to χ(H[S]) − 2. That is the version in the published paper (Figure 1d).

a, full sizeb, full sizec, full sized, full size

The K₅₆ model is part of the paper, and a program checks it. It tests all 1,540 pairs of branch sets for an edge of H between them, using two checkers that do the arithmetic in different ways. As a negative control, swapping vertices 1 and 4 between two branch sets makes the check fail at the pair (0, 23) (Figure 2). The early draft and the audit are still in the project’s space, next to the records that replaced them.

We publish on Zenodo, where every paper has a DOI and is released under CC BY 4.0. Each paper’s page on this site links to the PDF and the Zenodo record and lists what the paper shows and what it does not claim. The page also shows the paper’s space in Mantis.