Report · first published here September 22, 2026

A checked result, saved once and used twice: an engineering test of September 13, 2026

On September 13, 2026 a session of OpenAI's Codex agent built a tool that computes one exact piece of linear algebra, saves it with a certificate, and lets later checks verify the certificate before using it. In a registered seven-case test the two later checks each verified and reused the saved result, damaged copies were refused, and reuse was slower than recomputing. No part of the running loop calls the tool.

verification
reuse
engineering test

What Hypnos is

Hypnos is a research harness run by one person, its owner, and built so that small open AI models on the owner's own graphics cards do the looking in hard mathematics and frontier models do the expensive step, deriving something new and checking it. Its loop has run since August 11, 2026, with pauses between runs: three small models read a growing notebook of mathematics one or two entries at a time and write one-line candidate ideas; code filters and queues the lines, and Claude Opus 5, a frontier model made by Anthropic, reads batches drawn from the queues, keeps the few it judges worth a closer look, and writes each of those into the notebook as a new entry. The rest happens in sessions the owner starts by hand with Claude Fable 5.1 (Anthropic) or GPT-6 Astra (OpenAI): they do that expensive step, and the four mathematics papers published here were written in such sessions, each at the owner's direction, each reviewed by the other company's model, and as of October 3, 2026, read by no human mathematician. How Hypnos works, step by step

Can a checked result be saved once and used again, with each use verified rather than merely cited? For one exact lemma, in a test of September 13, 2026, it could. GPT-6 Astra (OpenAI) built the tool and the test at the request of the owner, the person who runs Hypnos, in a session of OpenAI's Codex agent, the command-line program through which that model runs. None of it was the loop's work: the test made no model calls, and the session wrote its inputs. The day before, that session had reviewed Hypnos and found no reliable route from a checked result to further work: the execution step, which turns an entry's runnable check into a program, saw the entry's description but not the earlier results it built on.

The piece of mathematics

Take distinct integer positions j, each with a value u_j = ±1, and let W be the symmetric matrix with W_jk = 4π²(-1)^(j-k)(u_j - u_k)/(j - k) for j ≠ k and zeros on the diagonal. Its inertia counts its negative, zero and positive eigenvalues; its nullity counts the zero ones. The lemma: with p positions at +1 and q at -1, W has inertia (min(p,q), |p - q|, min(p,q)).

Proof. Multiplying row and column j by (-1)^j removes the factor (-1)^(j-k), dividing by 4π² changes no sign, and entries between equal values vanish, so listing the +1 positions x_a before the -1 positions y_b gives zero diagonal blocks and off-diagonal blocks C and Cᵀ, with C_ab = 2/(x_a - y_b). C is a Cauchy matrix of rank min(p,q): if p ≤ q, a dependence among its rows would give a rational function whose numerator, of degree at most p - 1, vanishes at the q points y_b, so all its coefficients vanish; if p > q, transpose. Each nonzero singular value of C gives one positive and one negative eigenvalue, and the other |p - q| directions are zero.

For positions 0 to 6, the first five at +1 and the last two at -1, C has rows (-2/5, -1/3), (-1/2, -2/5), (-2/3, -1/2), (-1, -2/3), (-2, -1); its first two rows have determinant 4/25 - 1/6 = -1/150, so C has rank 2 and the inertia is (2, 3, 2). The ingredients (Cauchy matrices, rank, and the eigenvalue pairing of a symmetric matrix with zero diagonal blocks) are standard, and the September 12 review calls isolating this lemma an application of method, not a claim of a new mathematical result.

W is the derivative, at zero displacement, of a quadratic form an earlier program of the execution step had computed: a sum of squared transform values at points near the integers, compared with 4π² times a squared norm. On September 1 to 2, 2026, a fresh session of Claude Fable 5.1 (Anthropic) derived it in closed form and found one row of that program's table was a floating-point rounding artifact.

The tool and the test

A producer saves C exactly, with a rank witness (a determinant of part of C modulo a large prime), as a certificate named by the SHA-256 digest of its bytes, which shows only that a file is the intended one. A separate consumer re-checks every entry, recomputes the witness by another method, and reads off the inertia only if the two agree and are nonzero.

The comparison was registered, that is, written down and fixed, before it was taken: five valid cases (sign patterns on 5 to 129 positions), each with two later questions (the full inertia and the nullity), and two invalid controls (a repeated position, a value other than ±1). One side rebuilt the certificate for each question; the other built it once for both.

Both sides completed all ten valid questions with the inertias the lemma predicts; the reuse side verified the saved certificate each time and ran the producer seven times, not fourteen. In ten more controls the saved certificate was removed or corrupted, and every consumer refused to complete. Reuse was slower, 1.812 seconds against 1.500, because checking dominated so small a workload; no speed claim had been registered.

What it does and does not show

The two questions are closely related, within one narrow family of tools. It does not show a speedup, an improvement in any AI model's ability, or a discovery made by Hypnos on its own. The tool was added to the harness's code on September 14, 2026, but as of October 2, 2026 nothing in the running loop calls it, and no comparison has been registered in which the execution step would use checked work. The report on the build names the next question: whether checked work removes another task's obstacle at a useful total cost. A worked case lays the test out step by step.