/solve-maths-mem · design (proposal)

/solve-maths with a MemGPT memory

Same root, same ≤ 9 agents, same rounds. The only change: the root's state moves out of its context into three tiers it pages with five functions, after MemGPT [Packer et al.].

Why: what the root must remember

To continue a run, the root needs three things it wrote itself. In satake-two-levels:

registry · R-1, 02:56

central inertia     settled
  SL₂/SO₂ fails at both levels
convolution fibres  running
  GL₄/Sp₄ settled at both
trace dictionary    settled
  (SG) over F_q((t)) ⇒ sheaves
triangularity       running
restriction map r   settled
  E₆/F₄: r not onto

then

next action · R-1, 02:56

A7: audit every candidate
    proof (A2, A4, A6 now;
    A1, A3, A5 on return)
A8: attack the E₆/F₄ sheaf
    level by the fibre method
agents in use: 8 of 9

later

verdict draft · R-4, 04:16

Every row agrees at both
levels except E₆/F₄:
  sheaves    C^Sat = C
             (A8, audited)
  functions  H_K·φ₀ ⊊ C_K
             (A6, under (A))
No case the other way round.

Registry: every approach with its state and the step ids behind it. Next action: whom to launch or redirect, with what brief. Verdict draft: the answer as it would be stated now.

Timeline 02:02 to 04:16 UTC: the root's context holds the registries R-1 to R-3 and the verdict draft R-4; agent A7's context ends at each return; returns are written to disk as they arrive, tree.json and verdict.md only at Record; the proposed core.md is checkpointed at R-1, R-2, R-3, R-4. A dashed line at 03:48 marks a lost session: the two contexts are lost, the files and core.md survive. — Until Record, the three live only in the root's context; with core.md, a lost session costs at most the work since the last checkpoint.

Across runs: iwahori-two-levels (18 Oct) received the satake-two-levels verdict and propositions as hand-picked references; the steps, dead ends and audited errors behind them were not searchable. Source of the figure: figures/make_mem_figures.py.

Memory in other designs.
design	memory
Hearsay-II [Erman et al.]	a blackboard every module reads and writes
Anthropic research system [Anthropic]	the lead agent saves its plan to an external memory before its context fills
MemGPT [Packer et al.]	tiers paged in and out of the context, like virtual memory
Generative agents [Park et al.]	a stream of every experience, summarized into reflections

MemGPT in one definition

(memory hierarchy) [Packer et al., §2]

Context window of $c_{\max}$ tokens; main context and external context:

$$\underbrace{\mathrm{sys}\ \oplus\ W\ \oplus\ Q}_{\text{main context},\ \le c_{\max}}\qquad\underbrace{\mathrm{Recall}\ \cup\ \mathrm{Archive}}_{\text{external, paged in by function calls}}$$

$\mathrm{sys}$ read-only instructions; $W$ a fixed-size read/write text block, written only by function calls; $Q$ a FIFO of messages whose head is a recursive summary; Recall holds every message, evicted ones included; Archive is a read/write store of texts.

(queue manager, function executor) [Packer et al., §2.2–2.4]

$$|\text{main}|\ge 0.7\,c_{\max}\ \Rightarrow\ \text{warning};\qquad |\text{main}|\ge c_{\max}\ \Rightarrow\ Q\ \xrightarrow{\ \text{evict}\ \approx 0.5\,c_{\max}\ }\ \mathrm{Recall},\quad \mathrm{head}(Q)\leftarrow\mathrm{summ}\big(\mathrm{head}(Q),\ \text{evicted}\big).$$

0.7 and 1.0 are MemGPT's example values. Function calls are parsed and run; errors return to the model; retrieval is paginated. A call with request_heartbeat chains another step; otherwise the model yields until the next event.

Limit [§3.2.1]: MemGPT often stops paging before exhausting the retrieved results, and embedding search caps document QA.

From MemGPT to a solve run

MemGPT's Recall and Archive hold text. A solve run needs more: what was said, in order, and what is known, with the hypotheses it holds under. Let $G=(V,E)$ be the run record (overview).

(Recall: a log) [Packer et al., §2.2; Kreps]

$$\mathrm{Recall}_t=(e_1,\dots,e_t),\qquad e_i=(\text{time}_i,\ \text{actor}_i,\ \text{kind}_i,\ \text{ids}_i\subseteq V,\ \text{text}_i),\qquad \text{time}_1\le\dots\le\text{time}_t,$$ $$\text{kind}\in\{\text{source},\ \text{brief},\ \text{return},\ \text{registry},\ \text{redirect},\ \text{audit},\ \text{correction},\ \text{checkpoint},\ \text{evict}\}.$$

The only write is append, $\mathrm{Recall}_{t+1}=\mathrm{Recall}_t\cdot e$; so $\mathrm{Recall}_s$ is a prefix of $\mathrm{Recall}_t$ for $s\le t$, and a mistake is corrected by a later event. Briefs and returns are kept whole as files; their events point to them.

(Archive: a graph of steps) [Massot; Farmer et al.]

$$\mathrm{Archive}=(D,G,\mathrm{rec}),\qquad d=(\text{id},\ \text{origin: path or URL},\ \text{retrieved},\ \text{hash},\ \text{text})\ \ (d\in D),$$ $$ \mathrm{rec}(u)=\big(\text{statement},\ \mathrm{hyp}(u),\ \sigma(u),\ \text{parents},\ \text{proof},\ \st(u),\ \text{audit}\big)\quad(u\in V),$$ $$L\subseteq\textstyle\bigsqcup_r V_r,\qquad \text{kind}(u)\in\{\text{lemma},\ \text{dead end (with the missing statement)},\ \text{error (with the failed input)}\}.$$

$D$ is the read-only store of sources (the problem's files and webpages, snapshotted when fetched); a step that cites a source has it as a parent. Ids run/step are never reused. $\mathrm{rec}(u)$ changes only after an event about $u$ is appended to Recall (write-ahead [Mohan et al.]), so the Archive at time $t$ is determined by $\mathrm{Recall}_t$.

Each tier: what it contains, who writes it, how it is read.
tier	contains	written	read
$\mathrm{sys}$	SKILL.md; the Fix: statement, setting, criterion, checklist	once, at Fix	always in context
$W$	`memory/core.md`: phase, portfolio, open gaps, next, inputs; ids + one line	`core_set`, ≤ 2,000 tokens	always in context
$Q$	the root's messages, head = summary of the evicted ones	harness	in context until evicted
Recall	$e_1,\dots,e_t$ in `memory/events.jsonl`; `briefs/`, `returns/` verbatim	append only	`recall_search`, by id or keyword
Archive	sources $D$ in `sources/`; $\mathrm{rec}(u)$ for $u\in V$ in `tree.json`; $L$ in `solve/library.jsonl`	after an event; $L$ at Record (M2)	`archive_search`, `archive_get`

What an archive stores, and when reusing an entry is safe.
design	entry	reuse is safe when
MemGPT [Packer et al., §2.2]	a text passage	not checked
LEGO-Prover [Wang et al., §3]	a lemma Isabelle verified; failed statements in a separate store	the prover checks the new proof
LeanDojo [Yang et al., §5]	a Lean declaration	it is accessible (earlier in the file, or imported) and Lean checks the use
little theories, MMT [Farmer et al.; Rabe & Kohlhase, §3]	a theorem in the smallest theory where it holds	a view (theory morphism) maps its axioms to theorems of the target
/solve-maths-mem	$\mathrm{rec}(u)$ with $\mathrm{hyp}(u)$ and $\sigma(u)$	an auditor checks $\sigma_r\models\mathrm{hyp}(u)$ (M3)

Recall is episodic memory and the Archive semantic memory [Sumers et al., §4.1]. Without a proof checker, M3 plays the role of the view. Exercises: Recall and Archive.

The problem's files and webpages

Where each part of a problem's starting material lives.
item	tier	why
problem, setting, criterion	$\mathrm{sys}$ (the Fix)	fixed for the run
each file or webpage, full text	Archive, $d\in D$	long, read on demand; a webpage can change, so the snapshot is kept
“fetched $d_3$”	Recall, kind source	when it entered, and from where
the parts in use now	$W$: id + one line	e.g. “$d_2$ = Sakellaridis §5, assumptions (A1)–(A5)”
a passage being read	$Q$	evicted like any message

MemGPT does the same for document question answering: the documents sit in archival storage and are retrieved by function call [Packer et al., §3.2].

One of each, from satake-two-levels

$\mathrm{sys}$ · the Fix (excerpt)

problem    For the symmetric spaces of Table 1,
           is there one where sheaves generate
           but functions do not, or the reverse?
setting    k = C; G connected reductive, θ an
           involution, G^θ connected, X = G/G^θ
criterion  decide every row of Table 1 at both
           levels, with proofs, or name the exact
           statement that would decide it

$W$ · `memory/core.md` at 03:43

## phase       round 2 · 03:43Z
## portfolio   A1 literature · A2 SL₂/SO₂ · … · A6 E₆/F₄
## open gaps   E₆/F₄ at function level ← A5-9
## next        A7 (continued): audit A5-7, parents by id
## inputs      A2-4 audited · A5-7 not yet

$Q$ · the root's last messages

[summary] six agents launched 02:06; A6, A2,
          A4 returned; R-1: A7, A8 launched
[02:57] return  A3: symplectic family, A3-11
[03:10] return  A1: classification, A1-9
[03:32] return  A7: audit, A7-19
[03:32] root    R-2: registry after the audit

Recall · `events.jsonl`

{"time":"03:42","actor":"A5","kind":"return",
 "ids":["A5-7","A5-8","A5-9"],"text":"returns/A5.json"}
{"time":"03:47","actor":"A7","kind":"return",
 "ids":["A7-24"],"text":"A5-8 holds; A5-9 stale"}
{"time":"06:16","actor":"audit","kind":"audit",
 "ids":["A5-8"],"text":"error: input (a) fails,
  pair model, residue char. 2"}

Archive · `archive_search`

archive_search("GL2m/Sp2m generation",
               setting="F_q((t))")
[{"id": "satake-two-levels/A5-7",
  "status": "proved", "audit": "minor",
  "setting": "every non-arch. local F",
  "statement": "(SG) for GL2m/Sp2m …"},
 {"id": "satake-two-levels/A5-9",
  "status": "blocked", "audit": "minor",
  "statement": "E6/F4 at function level:
                what is missing"}]   page 1 of 2

Archive · `archive_get("…/A5-7")`

statement  H_K·φ₀ = C_K for GL2m/Sp2m, every m ≥ 1
hyp        F non-archimedean local
parents    A5-5, A5-6
proof      1. orbits ↔ symplectic Smith form …
status     proved
audit      minor: every step re-derived

$W$ holds ids and one line each; the proof comes back only with archive_get. Q's messages and the Recall times are from the run's record; the event file is the proposed format.

Architecture

Only the dashed box is new; the agents and rounds are those of /solve-maths.

Five functions

The root's only access to memory (`scripts/mem.py`); errors come back as text.
call	returns / does	who
`core_set(field, text)`	rewrites one field of $W$; refused if $\|W\|>2000$ tokens	root
`recall_search(q \| id, page)`	events, briefs, returns; 5 hits per page	root
`archive_search(q, setting, page)`	steps of this run and the library: id, statement, status, grade, setting, run; 5 per page	root
`archive_get(id)`	one full step: statement, hypotheses, proof, parents, audit	root; auditors, read-only
`archive_insert(id)`	copies an audited step to `solve/library.jsonl`	root, at Record

What memory may not do

Let $G$ be the run record, $L$ the library, $\sigma(u)$ the setting and $\mathrm{hyp}(u)$ the hypotheses of a step $u$, and $\sigma_r$ the setting of run $r$.

(memory invariants M1–M4)

$$\begin{aligned} &\textbf{M1 cache: } && \st_{W}(u)=\st_{L}(u)=\st_{G}(u)\quad\text{for every } u \text{ named in } W \text{ or } L,\\ &\textbf{M2 admission: } && u\in L\ \Rightarrow\ \st(u)\in\{\text{proved},\text{refuted},\text{blocked}\}\ \text{and}\ u\ \text{passed the audit, or was repaired},\\ &\textbf{M3 reuse: } && u\in L\ \text{cited in run } r\ \Rightarrow\ \sigma_r\models\mathrm{hyp}(u),\ \text{checked by an auditor of } r,\\ &\textbf{M4 bound: } && |W|\le 2000\ \text{tokens};\ \text{checkpoint at } 0.7\,c_{\max}\ \text{and at registry, redirect, handoff}. \end{aligned}$$

M1: a summary cannot promote a claim. M3 is the rule “no transfer by analogy” applied to the library: a lemma proved over $F_q((t))$ is not an input over a $p$-adic field.

Flow

Problem + references
├── Recall       archive_search(statement, setting) over the library:
│                  audited lemmas · dead ends with the missing lemma · known errors
├── Fix          as /solve-maths; write W = core.md
├── Portfolio    as /solve-maths; briefs may cite library ids as inputs or dead ends
├── Round 1      root yields; each return → returns/, tree.json, events.jsonl
├── Registry     built by paging the archive, not from the context; checkpoint W
├── Round 2      auditors read parents by archive_get(id); M3 checked here
├── Verdict      checkpoint W
└── Record       as /solve-maths; archive_insert every step that satisfies M2

Design choices

Root only. Agents keep their briefs; round 1 never sees the library, so independence (I1) is unchanged.
Id before embedding. Lookup by step id and keyword over plain files; MemGPT's own limit is retrieval quality and early stopping [Packer et al., §3.2.1].
Cache, not certificate. Status lives in tree.json; memory copies it (M1).
Library across runs. Only audited steps enter (M2), each with its setting; reuse is checked like any cited theorem (M3).
Checkpoint by events. Registry, redirect, handoff, and MemGPT's 70 % warning.
Plan in memory. The lead agent saves its plan before its context fills [Anthropic]; here the plan is $W$.

Test before use

Three checks on existing runs, before any new run uses the memory.
test	pass if
resume: stop satake-two-levels after its registry R-1; restart from `core.md`	same next action; every blocked route found
reuse: Fix of iwahori-two-levels with the library of satake-two-levels	its audited inputs and dead ends returned, each with its setting
status: `mem.py check` on the library	M1–M2 hold: 0 promoted statuses

$$N_{\text{mem}}=N_{\text{solve-maths}}\le 10,\qquad \Delta\text{tokens per root turn}\le |W|+5\ \text{hits}.$$

Files the skill would add

.claude/skills/solve-maths-mem/   (= .agents/skills/…)
  SKILL.md                = solve-maths + Recall step,
                            checkpoints, M1–M4
  references/
    memory-protocol.md    tiers · functions · core.md template
  scripts/
    mem.py                core_set · recall_search ·
                          archive_search · archive_get ·
                          archive_insert · check
  reuses solve-maths/references/, tree_md.py

<slug>/              as /solve-maths, plus
  memory/
    core.md           W, latest checkpoint
    events.jsonl      t · actor · action · ids · reason
solve/
  library.jsonl       one line per audited step:
                      run · id · statement · setting ·
                      hyp · status · grade · repair

Status: proposal. Not built; the installed /solve-maths and its schemas are unchanged.

/solve-maths with a MemGPT memory

Why: what the root must remember

registry · R-1, 02:56

next action · R-1, 02:56

verdict draft · R-4, 04:16

MemGPT in one definition

From MemGPT to a solve run

The problem's files and webpages

One of each, from satake-two-levels

\(\mathrm{sys}\) · the Fix (excerpt)

\(W\) · `memory/core.md` at 03:43

\(Q\) · the root's last messages

Recall · `events.jsonl`

Archive · `archive_search`

Archive · `archive_get("…/A5-7")`

Architecture

Five functions

What memory may not do

Flow

Design choices

Test before use

Files the skill would add

tier	contains	written	read
\(\mathrm{sys}\)	SKILL.md; the Fix: statement, setting, criterion, checklist	once, at Fix	always in context
\(W\)	`memory/core.md`: phase, portfolio, open gaps, next, inputs; ids + one line	`core_set`, ≤ 2,000 tokens	always in context
\(Q\)	the root's messages, head = summary of the evicted ones	harness	in context until evicted
Recall	\(e_1,\dots,e_t\) in `memory/events.jsonl`; `briefs/`, `returns/` verbatim	append only	`recall_search`, by id or keyword
Archive	sources \(D\) in `sources/`; \(\mathrm{rec}(u)\) for \(u\in V\) in `tree.json`; \(L\) in `solve/library.jsonl`	after an event; \(L\) at Record (M2)	`archive_search`, `archive_get`

item	tier	why
problem, setting, criterion	\(\mathrm{sys}\) (the Fix)	fixed for the run
each file or webpage, full text	Archive, \(d\in D\)	long, read on demand; a webpage can change, so the snapshot is kept
“fetched \(d_3\)”	Recall, kind source	when it entered, and from where
the parts in use now	\(W\): id + one line	e.g. “\(d_2\) = Sakellaridis §5, assumptions (A1)–(A5)”
a passage being read	\(Q\)	evicted like any message

call	returns / does	who
`core_set(field, text)`	rewrites one field of \(W\); refused if \(\|W\|>2000\) tokens	root
`recall_search(q \| id, page)`	events, briefs, returns; 5 hits per page	root
`archive_search(q, setting, page)`	steps of this run and the library: id, statement, status, grade, setting, run; 5 per page	root
`archive_get(id)`	one full step: statement, hypotheses, proof, parents, audit	root; auditors, read-only
`archive_insert(id)`	copies an audited step to `solve/library.jsonl`	root, at Record

/solve-maths with a MemGPT memory

Why: what the root must remember

registry · R-1, 02:56

next action · R-1, 02:56

verdict draft · R-4, 04:16

MemGPT in one definition

From MemGPT to a solve run

The problem's files and webpages

One of each, from satake-two-levels

\(\mathrm{sys}\) · the Fix (excerpt)

\(W\) · memory/core.md at 03:43

\(Q\) · the root's last messages

Recall · events.jsonl

Archive · archive_search

Archive · archive_get("…/A5-7")

Architecture

Five functions

What memory may not do

Flow

Design choices

Test before use

Files the skill would add

\(W\) · `memory/core.md` at 03:43

Recall · `events.jsonl`

Archive · `archive_search`

Archive · `archive_get("…/A5-7")`