Vibe-coding a memory tool into a 130-year-old open problem

A August 2026 Substack essay by a writer using the handle "arbusto em chamas", narrating a few months of trying to vibe-code a memory tool for their coding agents and discovering that the feature they wanted most rests on an open problem in philosophy of language vibe-coding-agent-memory-abyss. It is a first-person confession rather than an analysis, and its value is as a case study in where cheap code stops helping.

What was built

The author came to LLMs recently, ramped up through Claude and then Claude Code, and by their own account spent weeks in a haze on a Max x20 plan, XY-questioning their way to what they took for solutions. The goal was a local, fast memory database that stores what agents learn and reloads it every session, rather than relying on prose files. An agent wrote most of it under direction: a Rust daemon, a rule that facts are never deleted but only superseded so the bank remembers what it used to believe, and four retrieval strategies fused and reranked by small local models. The author's honest read of the result is that they had built a search engine over a weird corpus and mostly followed along while the agent implemented papers they had skimmed.

Then came the ambitious part: automatic contradiction detection. A memory bank accumulates months of extracted facts, some stale, some wrong, and a memory that contradicts another without explanation is worse than none, because it pollutes the context window. "Can't be that hard." The design grew a "reasoning council" (abduction proposes, deduction certifies, induction learns rules), Agda proofs later ported to Cubical Agda, a machine-checked four-valued Belnap lattice distinguishing "not recorded" from "contradicted", a Petri net of every subsystem, and a plan language whose replay properties were proved before its parser existed. The author admits to having a solver, a proof assistant, and the faintest idea of what was happening.

The wall

Months in, the tool stores and classifies memory but does not do the one thing it was built for: it does not flag contradictions. Pushing Claude to encode prose memories into Answer Set Programming automatically, the author got the explanation that you cannot, because it is an unsolved problem in knowledge representation that Claude called "proposition identity". Stripped of the model's confident register, the problem is this: the conflict rules fire on syntactic equality of atoms, so the solver never judges whether two memories contradict — that judgment was already made, earlier, by whatever decided two stretches of prose map to the same atom. As the author restates it after a philosophy-of-language semester: deciding when two sentences express the same proposition is genuinely hard. Merge fact-atoms too eagerly and the checker invents conflicts. Their fallback hope, that a large enough bank would at least surface self-contradictions ("the current king of France is bald" versus "rocking a mohawk"), runs straight into Russell's point that there is no king of France at all. Claude dated the problem to Frege's 1892 "On Sense and Reference" and told the author they probably would not crack it either, at which point they stopped prompting for code and wrote the post.

The essay ends with the reading list the model produced: SEP entries on propositions and structured propositions, Frege, Quine's Word and Object, hyperintensionality as the modern keyword; McCarthy on formalizing context and CYC's microtheories on the knowledge-representation side; the applied names under which the problem is studied (open knowledge base canonicalization, cross-document event coreference, previously-fact-checked claim detection); and the LLM+ASP line (s(CASP), STAR, distilling ASP rules from LLMs).

How it sits in the vault

This is the negative-space companion to memoryfields, which appears in the same 2026 wave of agent-memory writing. Paterson's thesis there is that memory should be data with as little machinery as possible between the agent and it — no contradiction pipeline, no reasoning layer. This essay is what building that machinery looks like: the author tried to add exactly the automated reasoning Paterson says to leave out, and the reasoning is where it broke. The two do not cite each other, but read together they make one argument from both ends — memory-as-data is tractable, and the pipeline the author reached for is not, at least not the automatic-contradiction-detection part of it.

Inside the vault the problem already has a page. memory-conflict-detection describes detecting a new memory that contradicts an old one and keeping both visible; this essay is the report that the detection half, done automatically, is the hard part, because deciding two memories are about the same thing is proposition identity. The vault's own answer is the human-arbitration and lint-workflow path in that page, not an automatic checker — llm-wiki-as-agent-memory argues that a hand-editable markdown store makes the conflict problem much easier precisely because a person resolves it. agent-memory-components places the difficulty at the store's "contradiction decision" layer and notes it is where most libraries under-invest; this is the account of trying to over-invest there and finding no bottom.

More broadly it is a vibe-coding cautionary tale in the family of building-syntaqlite-ai: the agent produced a compiling, tested, even machine-proved implementation of a design the author did not understand and could not finish, which is peril-of-laziness-lost and the skill-atrophy-supervision-paradox shown from the inside. neurosymbolic-ai is the sober frame for the LLM+ASP approach the author was chasing, and llm-self-verification-limits is the reason the "reasoning council" of one model checking another was unlikely to close the gap.