[zibo-yang]

Problem

The search-and-reuse mechanism landed across #171, #204, #211, #311, #319, #343 and facebookresearch/atlas-lean#164, but its design, trade-offs and evidence live only in those PR threads. A user browsing the repository cannot find the reasoning in one place.

Changes

• docs/papers/search-and-reuse/: the paper Search Before You Prove: Verified Retrieval and Reuse of Shared Lean Libraries in Multi-Agent Autoformalization as a PDF (135 KB).
• README.md: a short "Search and reuse" section after "Blueprint model" that says what the mechanism does and links to the paper.

No code, skill or test changes.

What the paper contains

• The design: blueprint search, the library index format and its digests, the generator and its Lean probe, the reader that verifies an index from files alone, publication on a tag, project new --library, and the agent rules.
• An evaluation on the index ATLAS published at autoform-index/64c2773ffad3:
  • cost: a library search takes 1.14 s end to end, of which verification is 366 ms;
  • a known-item study: 4,005 queries over 801 declarations, 100% recall;
  • a replay of 103 queries that agents issued in trial sessions;
  • the trial outcomes recorded in the PRs above.
• Limitations, including the deferred findings from the Search a shared Lean library, generate its index, and teach the skills to reuse it (#203) #204 reviews, and three matching defects the replay found (hyphenated terms, short-term substrings, proper names).

Verification

• The README link resolves to the committed PDF.

🤖 Generated with Claude Code

[Deicyde]

Review at 8535561

Thanks, Zibo. Linking the paper from the README is useful, because the search-and-reuse design is otherwise spread across #203, #204 and #311. The paper's numbers check out against ATLAS's published index: 2,257 modules, 11,649 declarations and 10,053 docstrings. The code also agrees with the paper on the 64 MiB cap, the tree digest, the locked-revision check and the CLI contracts. A few things should change before merge.

Verdict: request changes.

1. The commit message describes a file that isn't there. c963cae says "The PDF and its LaTeX source live under docs/papers/search-and-reuse/", but only the PDF is committed. With a merge commit, that sentence would land in main's history. Either commit the source, or squash and drop the sentence. Squashing also drops the first PDF blob; the history currently holds two full copies.

2. The README overstates what agents search.

   • "Any shared Lean library the project depends on": agents search only libraries that publish an Autoform index. The catalog in autoform_cli/project/libraries.json lists only ATLAS today, and other dependencies are skipped and reported as unchecked (skills/formalize/references/library-search.md).
   • "Checked against the exact library version the project builds with" claims more than the reader checks. It compares the checkout with the revision lake-manifest.json locks, and a package replaced with lake --packages= is not detected (autoform_cli/README.md:1309).

   Suggested replacement, which also fixes the 166-column link line:

   ## Search and reuse
   
   Before adding a result, agents search the blueprint and every library the
   project depends on that publishes a search index, such as
   [ATLAS](https://github.com/facebookresearch/atlas-lean), and reuse what
   already exists. An index is used only after it is checked against the commit
   the project locks. The [search contract](autoform_cli/README.md#search-contract)
   is the reference. The paper
   [*Search Before You Prove*](docs/papers/search-and-reuse/search-and-reuse.pdf)
   (October 2026) explains the design and evaluates it on ATLAS's published
   index.

3. The acknowledgments thank two of the listed authors. The second commit added five co-authors, but page 12 still thanks two of them by their GitHub handles. Drop or reword those thanks and rebuild the PDF.

4. Where the PDF lives is a maintainer decision.

   • It would be the repository's first binary file and its first docs/ directory.
   • Its source isn't in the repo, so its text can't be reviewed or corrected here.
   • Every plugin install downloads it.
   • Committing it puts the paper under the repository's MIT license (CONTRIBUTING.md), so every author should be fine with that.

   If it stays in the repo, commit the .tex and .bib files with it. Otherwise, link a hosted copy, such as arXiv or a release asset, and make this PR README-only.

5. PR body (nit):

   • "Its design, trade-offs and evidence live only in those PR threads" isn't quite right. The design is documented in the CLI reference's search contract and in the library-search reference; only the trade-offs and the evidence live only in the threads.
   • "100% recall" holds by construction, since every query word occurs in the target's docstring. The informative number is Hit@10, which rises from 25.3% with one word to 96.6% with five.

Checked:

• The branch merges cleanly into current main (a021c2a1), and CI is green.
• The README link resolves.
• The PDF contains no scripts, embedded files or local paths.
• The new section doesn't affect the README tests.

Posted by PR swarm: PR Swarm Lead