Paper Review Series: Anthropic's FLT Formalization and the Case for Shared State
On 4 September 2026, Anthropic reported that Claude had formalized Fermat’s Last Theorem in Lean in 11 days, working largely autonomously. Dozens of agents contributed to a proof containing 13 million lines of code. This was the formalization of an existing mathematical proof. The achievement was making its reasoning computer-checkable. Anthropic’s report
For this series, the most instructive detail is what happened before the successful run. Anthropic describes agents that:
“quickly lost track of the project’s state and stopped collaborating effectively.”
The successful effort used Prove2Me. Anthropic credits its dependency graph, separation of statements from proofs, and searchable theorem descriptions with improving coordination, compilation, and reuse. Source
The Prove2Me paper by Chen and colleagues, published on 28 August, explains the platform behind that result. We read the two together as an architectural case study. Neither is a controlled comparison of retrieval systems or memory products.
The question they raise is practical: what do collaborating agents need beyond access to their previous work?
1. Retrieval finds evidence; shared state records what has been accepted
Section titled “1. Retrieval finds evidence; shared state records what has been accepted”Consider two questions an agent might ask:
- Which existing results could help with this proof?
- Which prerequisites of this proof remain unresolved?
The first is a discovery problem. The second requires an accurate representation of the project’s state.
A retrieval system might surface a promising theorem, an earlier proof attempt, and a discussion of a missing assumption. The agent still needs to distinguish a suggested approach, an accepted contribution, and a completed proof.
Imagine this history:
An agent reports that attempt P is complete.The verifier rejects P.Another agent submits a corrected sketch Q.Q passes its check, conditional on an unproved lemma L.The useful state is precise: P was rejected; Q is a valid conditional contribution; the target is not yet fully proved through Q. Retrieving the observations does not automatically establish those distinctions. Something must interpret them under the application’s rules.
That interpretation can happen during every read, or the system can maintain its result for all agents to use. An event log with a deterministic projection can do this too; maintaining state does not require discarding history or overwriting records.
A retrieval-augmented generation (RAG) pipeline can retrieve structured records, and a graph can serve as a system of record. The question is where accepted state is maintained and what rules govern it.
Here, “accepted” means accepted under the system’s evidence and validation rules. A stored status is only as reliable as the process that establishes it.
2. Prove2Me gives shared objects a precise contract
Section titled “2. Prove2Me gives shared objects a precise contract”The paper describes immutable theorem statements, stored separately from their proofs. Multiple proofs can target one statement, with submissions checked against that target in a pinned verification environment. Paper, section 3
This gives agents a stable object to coordinate around. One agent can work on a proof without silently changing the proposition another agent is trying to use.
A proof-sketch can establish a target conditional on imported statements that remain unproved. The platform tracks those dependencies; completion propagates when the necessary children are closed. Curated milestones help agents converge on compatible formalizations. Paper, sections 4.2–4.4
The dependency edge has operational meaning: it changes what work remains open and when a result can count as complete. A graph of related text would not supply that meaning by itself.
The architectural lesson is to define stable objects, specify what contributions mean, and establish how accepted contributions change shared state.
Immutability also needs a lifecycle. Prove2Me’s current documentation says published formal content stays fixed, while corrections use deprecation and replacement; descriptive metadata remains editable. Deprecating a proof can reopen work in the decomposition graph. Prove2Me FAQ
This distinction matters outside mathematics too. Some domains need permanent versions; others need a current assignment or preference that can change. Persistence alone does not choose the right policy.
3. The reusable opportunity sits above storage
Section titled “3. The reusable opportunity sits above storage”None of this requires a new database category. A graph is a natural representation for dependencies, and conventional databases plus application code can implement the relevant integrity rules.
But several different responsibilities have to come together:
| Responsibility | Question it answers | Example |
|---|---|---|
| Structure | What can be represented? | An attempt has at most one target. |
| Interpretation | What does this observation refer to? | This message concerns attempt Q, not a new attempt. |
| Acceptance | Is the proposed change justified? | A trusted verifier accepted Q under the recorded assumptions. |
A uniqueness rule can prevent duplicate identifiers. It cannot, by itself, decide whether differently expressed mathematical statements should share an identity. An allowed-value rule can restrict a status vocabulary. It does not establish the evidence required for a transition.
A capable team can implement these responsibilities using database constraints, application code, extraction models, and external validators. Prove2Me is a case where substantial domain-specific engineering is appropriate.
The opportunity for memory infrastructure is to make recurring work reusable: extracting objects, matching identities, normalizing values, and interpreting relationships. Developers could then spend more of their effort on the acceptance rules specific to their application.
That is the connection to xmemory: a higher-level way to specify how observations become persistent state.
4. XMD makes part of the memory contract programmable
Section titled “4. XMD makes part of the memory contract programmable”XMD, the xmemory Model Description format, combines typed objects and relationships with descriptions supplied to the extraction pipeline. Those descriptions can define object boundaries, distinguish similar fields, specify normalization, and explain what evidence supports a relationship.
Names and types rarely contain enough information. A field named status does not explain whose report determines it. A relationship called depends_on does not distinguish a formal prerequisite from a potentially useful technique.
Consider this illustrative memory view around a proof-verification workflow. It assumes that trusted platform events supply stable theorem and attempt references on every relevant write:
xmd_version: v1
objects: Theorem: fields: reference: type: str required: true description: Platform-issued theorem reference; copy exactly. primary_key: [reference]
ProofAttempt: fields: reference: type: str required: true description: Platform-issued attempt reference; copy exactly. verdict: type: str enum: [pending, accepted, rejected] description: > Verifier-reported outcome for this attempt. Agent confidence is not verification evidence. Accepted does not imply that dependencies are proved. primary_key: [reference]
relations: targets: description: Connect an attempt to the theorem explicitly identified as its target. objects: attempt: {type: ProofAttempt, on_delete: cascade} theorem: {type: Theorem, on_delete: cascade} keys: one_target_per_attempt: [attempt]The primary keys specify record matching, the enum defines the extraction vocabulary, and the relation key expresses at most one target per attempt. The descriptions guide interpretation. These are documented XMD mechanisms.
This example represents attempts and targets. It does not implement Prove2Me, model the dependency graph, retain a full verification audit trail, or calculate theorem completion. Those responsibilities still belong to the surrounding workflow. The application must also reject writes missing the references assumed here; required: true alone does not guarantee their presence.
The useful abstraction is that a developer can change part of the memory pipeline’s behavior by changing the contract. For example, distinguishing “approved for deployment” from “successfully deployed” in a field description changes how those observations should map to state. Repeated mentions can update the same deployment record when they carry a stable reference.
This is what we mean by a memory programming language for the AI era: a declarative way to specify what agents should remember and how observations should map into that representation.
The phrase needs a boundary. Natural-language descriptions influence model-based interpretation; they do not have the deterministic semantics of a conventional program. A change to a description needs evaluation against representative inputs. It is a programmable policy, not a correctness proof.
The value is that decisions otherwise scattered across prompts, extraction code, matching logic, and storage operations become more explicit and inspectable.
5. A memory contract still needs evidence and enforcement
Section titled “5. A memory contract still needs evidence and enforcement”Writing “only accept a verifier-reported result” in a description does not authenticate the verifier, run Lean, or discharge a prerequisite. The surrounding system must control the evidence source and enforce the acceptance rules.
XMD’s documentation makes a related distinction: enum and required participate in extraction, but are not database-native CHECK or NOT NULL constraints protecting arbitrary out-of-band writes. XMD field semantics
Three questions remain separate:
| Reliability question | What must be checked? |
|---|---|
| Is the representation valid? | Values, identifiers, and relationships fit the contract. |
| Is the interpretation supported? | The source justifies the extracted claim or update. |
| Is the claim independently verified? | An authoritative system has established the relevant fact. |
A type check can answer part of the first question. It cannot answer all three.
Even formal mathematics preserves this boundary. Lean verifies a formal statement under its definitions and axioms; humans still audit whether mission cores express the intended mathematics, aided in Prove2Me by an independent agent’s back-translation. Paper, section 3.3
In a deployment workflow, an agent saying “done” is a report. A successful result from the deployment system is different evidence. Memory can preserve that distinction, but storing the report in a typed field does not give it the deployment system’s authority.
There is also a limit to the analogy: many everyday facts have no Lean-like verifier. Preferences change, reports conflict, and sources arrive late. A general memory system needs policies for uncertainty, provenance, and supersession as well as structure. The small XMD example above leaves those policies to the application.
6. Discovery and accepted state belong together
Section titled “6. Discovery and accepted state belong together”Prove2Me retains search over natural-language theorem descriptions and asks agents to look for reusable results. Paper, section 4.3
Search identifies a candidate. A stable object establishes what it says. Verification and dependency tracking determine how it can be used.
Exploratory notes, discussions, and unsuccessful attempts can remain valuable alongside accepted state. A document assistant may mainly need retrieval; a collaborative execution system may need strict transitions. Many applications need both.
Our previous Paper Review examined external, programmatically addressable state and feedback around state changes in work from NVIDIA and Prime Intellect. Prove2Me sharpens the next question: once several agents contribute, who defines the meaning of a contribution and the conditions for accepting it?
The FLT result cannot isolate the benefit of any one mechanism: coordination, compilation, and reuse changed together. It also used substantial compute – Anthropic reports about six billion output tokens – so elapsed time alone is not an efficiency comparison. Anthropic’s report
Nor does this establish that a general-purpose memory product would outperform a specialized platform.
Our hypothesis at xmemory is that a meaningful part of the recurring work can become a reusable layer. Developers define domain objects, identity rules, relationships, and interpretation policy; a memory engine applies that contract, while domain systems retain responsibility for authoritative verification.
The practical test is whether this reduces implementation effort and state-management errors compared with a well-engineered application built directly on conventional storage, at acceptable cost and latency. Useful measurements include incorrect record merges, unsupported status updates, stale-state errors, and recovery after corrections. Anthropic’s result does not answer that product question for us.
It does make the architectural question concrete:
XMD is our approach to making part of that architecture programmable through a declarative memory contract.