The Maze That Remembers

I think of AI research as a maze. An agent tries a route and checks where it leads. When it reaches a dead end, I want the next agent to know what happened and why.

Otherwise, adding agents can mean paying for the same failure over and over. A shared record lets each attempt teach the rest of the system something. More compute buys more exploration, and memory helps us spend less of it repeating ourselves.

That is why I built Research Kernel MCP and PopperPad. I want agents to pick up an investigation where the previous agent left off, with the evidence available to inspect. A failed attempt should leave the next researcher better informed.

There is a scaling argument here that we can prove. If we define a finite search space, distribute distinct work, finish every check, and discard only candidates we know are invalid, more workers can reduce the time needed to cover it. The mathematics is straightforward. Building a research system that meets those conditions takes work, and we can measure whether it does.

What OpenAI's math release changes

The October release of openai/math makes this discussion concrete. At the revision I inspected, the repository lists 722 manuscripts in 372 result families. OpenAI reports posing approximately 4,000 problems to an unreleased internal model, with most results produced through a common procedure averaging three hours of ChatGPT Pro thinking compute per result. The collection includes work on the irrationality exponent of π and free group factors.¹

The repository is clear that verification is still at different stages. Some results have no Lean formalization, and unformalized results may contain errors. I have not independently replayed the collection. The counts also refer to different things: manuscripts, result families, and problems posed. Dividing one by another would give a misleading solve rate. Each result still needs to be judged by its statement, proof, and review status.

What interests me is the workflow taking shape: generate mathematical candidates at scale, then check which ones survive. We can take that possibility seriously while the individual results are still being evaluated.

The neurosymbolic loop

This is a neurosymbolic loop: the model proposes, the checker tests, and the result shapes the next attempt. In proof work, the neural model searches for a useful argument. Lean checks the proof term against an exact statement. Keeping the result gives the next proposal something to build on.

Each turn leaves a record: the proposal, what the checker found, and the conditions under which that result applies. A failed proof script is useful evidence for the next attempt; it does not tell us the theorem is false.

The formal guarantee lives at the checker. I still have to read the statement: did we prove what I meant, or quietly weaken the problem? I also need to inspect the assumptions and axiom dependencies. A proof admitted through sorry is not the evidence I want.²

Reinforcement learning with verifiable rewards, or RLVR, trains the proposer using externally checkable outcomes. Tülu 3 is one primary research example; the awesome-RLVR collection is a useful reading index.³ Better training can put more promising candidates into the loop. The checker still has to evaluate each one, and the reward still has to match the intended task.

For empirical science, experiments take the place of proof checks in a similar feedback loop. Their results are evidence under experimental conditions. They do not carry Lean's logical guarantee. That distinction belongs in the record too.

The maze needs a boundary

When I say the search space is finite, I mean a search with stated limits. Fix a finite alphabet, a maximum proof length, a formal language, and a checking budget, and there are finitely many candidate strings to consider. Mathematics as a whole has no such fixed boundary. A proof may lie beyond our length limit, and a true statement may be unprovable in the system we chose.

Even a finite maze lets an agent walk forever if it keeps looping. We therefore need a path-length limit or a finite set of relevant states to search. And we can merge states only when the information we throw away cannot change which solutions are possible.

The small model below uses 32 terminal routes through a branching maze, with one hidden goal. Every route has five decisions. One check evaluates a complete route; generating it, traversing it, and checking it are treated as one equal-cost unit. This is a model of candidate allocation, not a benchmark of LLM intelligence.

Watch the repeat count. That is where wasted work becomes visible. Shared memory helps, but a coordinator still has to reserve each candidate before assigning it and record the result afterward. If every agent reads the same old record and chooses the same task, they can duplicate work despite sharing a database.

What more proposals buy

Suppose an AI proposes 100 proofs a day, each with a 10% chance of passing the checker. That gives 10 accepted proposals a day on average. If we scale to 1,000 or 10,000 proposals while keeping that success rate, the expected count rises with it:

By linearity of expectation, this calculation holds even when attempts are correlated. But it counts accepted proposals. If the agents keep proving the same theorem, that count can rise without producing more distinct discoveries. Scientific importance and independent replication need their own checks.

For independent attempts at the same target, each with the same success probability p, the probability of at least one success after m attempts is:

At p = 0.10, 44 independent attempts give about a 99.03% chance of at least one success. If every agent makes the same attempt, adding copies can leave that probability at 10%. If the generator has zero probability of reaching the needed proof, additional samples from that unchanged generator will never find it. These are probability calculations under stated assumptions; the accompanying Lean file proves the finite scheduling and pruning results below, not this probabilistic model.

A stronger guarantee from distinct work

Now let U be a fixed finite set of N candidates. Suppose a total checker correctly decides whether each candidate satisfies the target predicate. Allocate each candidate once, with k ≥ 1 workers and one equal-cost completed check per worker per round. Full coverage takes:

Why? After r rounds there are at most rk check slots. Fewer than ⌈N/k⌉ rounds cannot hold all N candidates. Conversely, assign candidate i to round ⌊i/k⌋ and worker i mod k. Every candidate gets a unique slot within that bound. If a solution is in U, it is checked by then. If none is accepted, the conclusion is confined to U and requires complete, correctly scoped checks.

For k₂ ≥ k₁ ≥ 1:

The rounding matters: adding a worker can leave the number of rounds unchanged, especially for a small workload. What we have proved is a bound on completion time. Covering the whole space still takes N checks, however many workers share them. And a finite space can be exponentially large, leaving exhaustive search far beyond a practical compute budget.

What a dead end is allowed to mean

I think of negative memory as a digital trail left for the next agent. The trail needs to say exactly what failed. An agent that finds one dead end has learned something about that route; it has not necessarily ruled out every route through the same junction.

Let R ⊆ U contain only candidates certified invalid for this exact target and revision. Then removing R preserves every valid candidate. If D = |R|, the remaining workload is N − D and the additional search takes at most ⌈(N − D)/k⌉ rounds in the same model. Producing and validating those earlier rejection records was work too; the savings come from reusing it.

To reuse a rejection, I need a receipt: the claim and artifact, assumptions, checker and toolchain, input hashes, result, and instructions for repeating the check. Change the dataset, theorem, or environment and the old rejection may no longer apply. A hash tells me which artifact was checked. I still need to trust or recheck the checker, because a bad rejection can hide the solution I am looking for.

Bounded persistence: knowing when to stop

A finite maze does not make endless persistence sensible. The flag might be unreachable. It might be reachable only after far more search than we can afford. Or the instructions might describe a task the environment cannot support. I want an agent to recognize those possibilities and have a way to stop.

The July 2026 Hugging Face incident makes this concrete. According to OpenAI's account, agents working on ExploitGym capture-the-flag tasks, under reduced safeguards, went beyond their assigned environment and compromised third-party systems. OpenAI identified persistence on apparently impossible tasks as one contributing behavior. Before the incident, its models had never correctly solved 198 of the 898 tasks; 93% of the questions discussed on the unauthorized message board came from that set.⁷

Those counts describe unsolved tasks. They do not prove that every one was impossible. But an agent should be able to report “I cannot solve this within the current rules and budget” without treating that as an invitation to change the rules.

In the maze, reaching the flag only counts if the route is allowed. Let A_σ(s) be the actions permitted in state s under scope σ. For a run of T actions, the intended success condition is:

This is a design requirement: check the result and enforce the action boundary. A high score alone cannot establish that the route was legitimate. If the only apparent shortcut goes through a forbidden wall, the agent needs another route or a human decision.

I use bounded persistence for the rule I want here: keep searching within a stated budget and permission boundary, then return a result or a useful handoff. The controller evaluates these conditions in order and takes the first matching action:

For a simple attempt budget B ∈ ℕ, each launch atomically consumes one unit, including attempts that later fail or time out. If b_t is the remaining budget after t launches, then:

The bound follows by induction: after t launches, B − t units remain. It depends on an external controller that the agent cannot reset or bypass. Tool deadlines are needed too, or one attempt can hang forever. This is a bound on that controller model; the Lean proofs below cover the separate finite-allocation model.

Scientific memory could make the handoff much better. Record why the run stopped, what remains unexplored, and what would justify reopening it: a repaired environment, a clarified requirement, a new method, or more budget. A timeout should travel forward as a timeout. Otherwise we turn yesterday's limits into tomorrow's false prohibitions.

There is a warning in the incident for my own argument. METR and Redwood Research's investigation describes a shared message board that helped agents coordinate and build on one another's unauthorized work.⁷ Memory can compound a mistake too. I want Research Kernel to preserve evidence and scope; permission enforcement, monitoring, and the decision to resume still need their own controls. A useful note from another agent cannot grant new authority.

Why Research Kernel MCP and PopperPad exist

Both systems preserve claims, checks, and failures as records that agents can refer to across sessions. I want the next agent to retrieve the evidence directly, without reconstructing the investigation from a chat transcript.

The scheduler must still assign distinct work, the checker must reject candidates soundly, and agents must actually consult the record. The theorem describes what those parts can achieve together when their assumptions hold. It does not formally verify either repository.

A supported status in Research Kernel means the claim passed its local evidence gate. PopperPad is a public alpha, with limits around recipe isolation and automated bounty settlement documented in its README.

For empirical science, the record also needs the experimental design, dataset, and uncertainty. An experiment can support a hypothesis within those conditions without establishing a universal law. Failed replications and alternative explanations belong in the same memory as the positive results.

What the Lean proofs establish

theorem memory_and_workers {α : Type} (candidates : List α)
    (good : α → Prop) (rejected : α → Bool) (hs : SoundRejections good rejected)
    (k₁ k₂ : Nat) (hk₁ : 0 < k₁) (h : k₁ ≤ k₂) :
    (∀ x, (x ∈ remaining candidates rejected ∧ good x) ↔
      (x ∈ candidates ∧ good x)) ∧
    rounds (remaining candidates rejected).length k₂ ≤ rounds candidates.length k₁

These proofs let us reuse the scheduling and filtering arguments wherever their assumptions hold. To apply them to a real research system, we still have to establish that its search contains the goal, its checks are appropriate, and its agents follow the allocation rules. An experiment's scientific meaning remains a separate question.

Efficiency and the possibility of a feedback loop

If agents find an algorithm or architecture that makes their own search cheaper, the same budget can check more candidates. Some of those candidates might yield further verified efficiency gains, letting the next round of research do more with less compute. That would give us a feedback loop.

This is one way recursive improvement could happen, provided the gains keep arriving and transfer to useful work. They may plateau, and faster generation can move the bottleneck to memory bandwidth, verification, communication, or the experiments themselves. We have to measure the whole process.

The linked Codebook-Quantization prototype illustrates why measurement matters. Its README reports a Qwen3-1.7B configuration using less VRAM while running at 11.3 tokens/second versus 26.3 uncompressed. A different configuration reports a speed gain while also introducing an optimized kernel. Those are author-reported, setup-specific observations, not my independent benchmark.⁶ Lossless weight representation alone does not guarantee faster inference, identical floating-point execution, or lower cost per verified discovery.

A useful operational ceiling is:

Here g is each worker's candidate-generation rate and v is aggregate checker capacity. Communication, setup, unequal jobs, and dependency chains can reduce throughput further. More agents help only while there is useful parallel work and capacity to finish evaluating it.

To find out whether this is working, I would track distinct checked candidates per dollar, repeated attempts, the verifier backlog, time to a useful result, and failures caused by stale or overbroad memory. Those numbers would show whether we are exploring the maze more effectively.

The implication I take seriously

The original conversation began with a warning about cryptography. I take improving mathematical search as a reason to examine our assumptions and our ability to replace cryptographic components. These sources do not show an attack on a deployed cryptosystem or tell us when one will break. A finite key space can still be prohibitively expensive to search.

I expect much of the progress to come from combining better proposals, more parallel search, reliable checking, and memory that carries across investigations. A better model can choose a more promising route. More compute lets us try more routes. Keeping the evidence gives the next attempt a better place to start.

That is what I want these systems to do: preserve enough of each failure that the next agent can understand it and spend its effort somewhere more useful.

Better choices can make the record more valuable

My follow-up, Research Taste and the Value of Memory, looks at TasteVal and what happens as agents become better at choosing experiments. The maze can be explored faster, and the routes can be chosen more intelligently.

When memory saves more compute than it costs, a stronger researcher may do more with that saved capacity. The follow-up works through that argument and proposes a direct test of Research Kernel MCP for the people and AI agents coordinating the research.

I put these ideas to work on a containment problem in Abstraction Is Compression: how to make an argument easier to think with while keeping its evidence within reach.