/solve-maths-mem · exercises II
Recall and Archive
The two tiers outside the context: Recall, what happened, in order; Archive, what is known, by name [Packer et al., §2.1; Sumers et al.: episodic and semantic memory].
The two stores
Precise definitions: Recall and Archive on the design page. In short:
$$\mathrm{Recall}_t=(e_1,\dots,e_t)\ \ \text{append-only};\qquad \mathrm{Archive}=(V,E,\mathrm{rec}),\ \ E\subseteq V\times V\ \text{“is a parent of”, acyclic}.$$Best practice
| practice | source | here |
|---|---|---|
| a log: append-only, totally ordered by time | Kreps | Recall: correct by appending, never by editing |
| write-ahead: log the change before applying it | Mohan et al. | an event in events.jsonl before tree.json changes |
| inverted index; precision and recall of a search | Manning et al. | recall_search, archive_search, and how to test them |
| stable labels that never change meaning | Stacks project | step ids run/step, never reused |
| each result declares what it uses | Massot | parents in every record; the support is computable |
| prove in the smallest theory; reuse through an interpretation | Farmer et al.; Rabe & Kohlhase | store \(\mathrm{hyp}(u)\) minimal; reuse needs \(\sigma_r\models\mathrm{hyp}(u)\) (M3) |
| a library grows only with verified lemmas | Wang et al. (LEGO-Prover) | only audited steps enter \(L\) (M2) |
| retrieve only premises available at that point | Yang et al. (LeanDojo) | search filtered by setting and by time |
Recall
(a wrong event) misconception
Recall holds {"time": "03:42", "actor": "A5", "kind": "return", "ids": ["A5-8"], "text": "A5-8 proved"}. At 06:16 the audit finds A5-8 wrong. What does the root write?
A new event, appended; the 03:42 event stays as it was:
{"time": "06:16", "actor": "audit", "kind": "audit", "ids": ["A5-8"],
"text": "error: input (a) fails for the pair model, residue char. 2"}
The 03:42 event is still true as a record of what A5 returned. Editing it would erase why A7-24 (03:47), and through it R-3 (03:54), said what they said.
(replay) compute
The status of a step is a fold over Recall: start with nothing and apply the events in order. The events that touch A5-8:
03:42 A5 return A5-8 proved 03:47 A7 objection A7-24: "A5-8 holds" 06:16 audit audit A5-8 error (pair model, residue char. 2) 07:03 C correction C-4 proves the support bound for the pair model, every F
What did the record say about A5-8 at 04:00, and what does it say at 07:30?
04:00: proved, endorsed by A7-24 (the prefix ends at 03:47). 07:30: audit error, corrected by C-4. Because Recall is append-only, \(\mathrm{Recall}_{04:00}\) is a prefix of \(\mathrm{Recall}_{07:30}\), and both answers come from one file.
(which first?) predict
The root must record the 06:16 audit in both events.jsonl and tree.json, and the session may end between the two writes. Which order loses nothing?
The event first: the write-ahead rule [Mohan et al.]. If the session ends after the event, a restart replays it into tree.json. In the other order, tree.json says “error” with no event saying who found it, when, or why.
(did the search find it?) compute
Suppose archive_search("support bound, pair model") returns page 1 = A5-8, C-4, S3-2, A5-3, A5-10, and the relevant steps are A5-8, A7-24, C-4, S3-2, S3-4, S3-6. Compute precision and recall of page 1. Page 2 holds S3-4 and S3-6: what is recall after page 2?
A root that stops after page 1, MemGPT's observed failure [Packer et al., §3.2.1], misses S3-4, the corrected A5-8, and still misses A7-24 (it says “A5-8 holds”, not “support bound”). The design page's reuse test measures recall on known answers.
Archive
(what an error reaches) compute
Parents, from the run's record (rounds 1–2 and the root):
A5-10 ← A5-8, A5-7, … A7-24 ← A5-8, A5-10, … A7-25 ← A7-24, … R-3 ← A7-25, A5-7, A6-6 A7-32 ← A7-25, … R-4 ← A7-32, …
A5-8 is found wrong. Which steps have A5-8 in their support, \(u\) with \(\text{A5-8}\in\supp(u)\)?
Six steps, the verdict among them. Each must be re-checked, not marked wrong: the corrections found that the conclusions survived. Without parents in every record this set cannot be computed.
(may a later run cite it?) transfer
A5-8 was stored with setting “every non-archimedean local \(F\)”. Its proof needs input (a), which fails for the pair model of \(\mathrm{GL}_n/(\mathrm{GL}_p\times\mathrm{GL}_q)\) when the residue characteristic is 2. A later run \(r\) has \(\sigma_r\): pair model, \(F=\mathbb F_2(\!(t)\!)\). May \(r\) cite A5-8, and how should the record have been stored?
No: \(\sigma_r\not\models\mathrm{hyp}(\text{A5-8})\), so M3 refuses the citation. The record should list (a) among \(\mathrm{hyp}\), not a setting broader than the proof covers: state the result in the smallest theory where it is proved, and reuse it only after checking an interpretation [Farmer et al.]. A7-24 made exactly this mistake inside the run: it said “A5-8 holds” without checking (a).
(what enters the library) classify
Under M2, which of these enter solve/library.jsonl? (a) A2-4, proved, audit correct; (b) A5-8 as returned at 03:42, before any audit; (c) A5-9, blocked, with the missing lemma stated; (d) a heuristic remark; (e) A5-8 after the audit, with its error and C-4.
(a), (c), (e). Blocked routes and known errors are as useful to the next run as proved lemmas: they say what not to try and what is missing. (b) waits for its audit; (d) has no status the library can keep.
(Recall or Archive?) misconception
A7's message “I suspect A5-8 is fine but I did not check (a)” — where does it belong?
Recall. The Archive holds steps with a status set by the run's rules; a remark changes no status. Recall keeps it, so an auditor can later see that the doubt was raised and when.
Your turn: store a dead end
(exit task) construct
Write the library.jsonl line for A5-9: blocked, “\(E_6/F_4\) at function level: what is missing”. Which fields does a future run need in order to use it without reading the proof?
{"run": "satake-two-levels", "id": "A5-9", "kind": "dead end",
"status": "blocked", "audit": "minor",
"statement": "the method of A5-3–A5-7 reaches E6/F4 once this is proved",
"missing": "E6(O)-orbits on Q_N(F) are parametrised by Λ_S^+, and the
counts (T_λ∗φ₀)(x_μ) vanish outside an explicit finite set",
"hyp": ["F non-archimedean local"], "parents": ["A5-7"],
"later": ["S4-14"]}
The missing lemma, stated exactly, is what makes a dead end reusable; later points to a step that went further by another route (S4-14: two generators, modulo Axiom 2.2.1 over \(\mathcal O\)).
Previous: \(\mathrm{sys}\) and \(W\). Design: /solve-maths-mem.