# Why research-kit

research-kit came out of one research project, a series of papers with a Lean 4 library written over months with one coding agent, and every piece of it replaced something that had failed there.

- **The agent started every session cold.**
  It asked again about matters settled weeks before, and a roadmap written by hand was where answers went to drift.
  One parked item collected forty-two dated re-test lines before a ranked list replaced the triage, with a reason for each rank and a kill criterion fixed before the work.
- **Hand-edited state was the single largest source of drift.**
  A pool of ideas, a brainstorming file and a table of results each lagged behind what the project had actually done, and one entry cited a declaration the library did not have.
  Now a record changes state through the tool, which writes everything the new state needs, a finding must name evidence that a machine can resolve, and the check fails on a record that does not hold together.
- **Reading the records cost more than the research.**
  In eight of ten measured sessions the records were the largest thing the agent read.
  Now a session starts from a short generated summary and reads records by id, never the directory whole.
- **A citation stood on a paraphrase.**
  A subagent's retrieval report is testimony, not a read, and two "recent results" turned out to be withdrawn preprints.
  Now a card grades how far a work was read, a read a subagent made alone counts as unread, and a reference entry with no card fails the check.
- **A prover's report is a claim about the tree, not the tree.**
  One handback said nothing about two commissioned declarations that had not landed.
  Now the landing reads the built library first, and a document row is written from the landed proof, never from the plan that commissioned it.

Each of these became a check rather than a lesson.
The checks run offline as pre-commit hooks, each ends with a line saying what it did not look at, and the whole record is plain Markdown in git that you can read, grep and diff without the kit.