diff --git a/docs/research-plan.md b/docs/research-plan.md
new file mode 100644
index 0000000..37bdb58
--- /dev/null
+++ b/docs/research-plan.md
@@ -0,0 +1,148 @@
+# lean-bench: research plan and paper brief
+
+Written 2026-10-21. Status of the system is taken from the repo README and the project notes (rebuild of 2026-09-19). Conference dates were checked on 2026-10-21; items marked *unverified* come from aggregator sites or projections and must be re-checked against the official call.
+
+## 0. Where the project stands, honestly
+
+What exists: a working pipeline (page-level detection with quote-anchored spans, vision-OCR for font-mangled PDFs, Lean 4 formalization with one repair pass, Lean verification, type-indexed SQLite store with provenance). One book (587 pages), one 26-page verified run (89 items, about 3.4 items per page).
+
+What a reviewer will say today:
+1. No quantitative result. The only numbers are operational (CI time, OCR failure rate).
+2. `verified` means Lean accepted the statement, not that the statement says what the book says. The notes already admit "a well-formed statement of the wrong theorem passes every check".
+3. Detection is not reproducible (80 vs 89 items on the same range).
+4. One book, one LLM, no baselines, no human annotation.
+5. The source book is copyrighted, so the data cannot be released as built.
+
+The plan below turns each of these into the paper's contribution or removes it.
+
+## 1. Venue decision
+
+| Venue | Deadline | Fit | Verdict |
+|---|---|---|---|
+| **ACL 2027** (Kyoto, Aug 20-22 2027), via ACL Rolling Review | **ARR submission 4 Jan 2027** (official site); commitment and notification TBA; 8-page long paper | Resource / evaluation paper, NLP + autoformalization. Optional theme on LLM homogenization | **Primary target.** About 11 weeks from today |
+| ICML 2027 | Abstract ~16 Jan, paper ~22 Jan 2027 (*unverified*, projected from the 2026 cycle; official CFP not out, location South America) | AI-for-math ML audience; bar for a benchmark with no new method is high | Backup if the faithfulness method is strong |
+| IJCAI 2027 | ~4 / 11 Jan 2027 (*unverified*) | General AI | Not recommended |
+| ITP 2027 (Glasgow, ~Aug 2-7 2027) | Not published yet | Formal-methods audience; cares about Lean/Mathlib correctness | Good fallback for a trimmed version; watch for the CFP |
+| COLM 2027 | ~30 Mar 2027 (*tentative*) | LLM-centred | Fallback if ACL misses |
+| NeurIPS 2027 Datasets & Benchmarks | ~14 / 21 May 2027 (*projected*) | Natural home for the full benchmark | Fallback with a full year of extra experiments |
+
+Already closed, so not options: ICLR 2027 (25 Sep 2026), CPP 2027 (10 Sep 2026), NAACL 2027 / COLING ARR cycle (12 Oct 2026), AAAI-27, NeurIPS 2026.
+
+**Recommendation:** target ACL 2027 on the 4 Jan ARR deadline. The work is a resource-plus-evaluation paper, which ACL accepts, and the date is official. Keep ICML (about 22 Jan) as a one-to-two-week-later alternative only if the experiments in 4.3 show a clear method gain. If ARR reviews arrive weak, commit to a later cycle or retarget NeurIPS D&B 2027.
+
+**What the ACL bar requires** (so the plan is built around it): a clear contribution beyond engineering; a meaningful evaluation with baselines and more than one model; human evaluation or annotation with agreement statistics; released artefacts that can be used (data and code, licence-clean); Limitations section and Responsible NLP checklist; reproducibility details; 8 pages double-blind.
+
+## 2. Paper framing
+
+**Working title:** *Compiled is not Faithful: Measuring and Closing the Fidelity Gap in Textbook-to-Lean Autoformalization*
+
+**One-sentence claim:** Lean acceptance badly overstates the quality of LLM autoformalization of real textbook mathematics; we release a page-grounded benchmark with human fidelity labels, show how large the gap is across models and pipeline stages, and show that a cheap round-trip fidelity check shrinks it.
+
+Contributions (all must be evidenced in the experiments):
+1. **lean-bench**, a page-grounded benchmark of textbook items (statements, definitions, exercises) with Lean 4 formalizations, each carrying source hash, page and character span, and human fidelity labels.
+2. **A measurement of the verified-vs-faithful gap** by model, by item type, by domain, and by pipeline stage (OCR, detection, formalization, repair).
+3. **A fidelity filter** (round-trip informalization plus judge ensemble, calibrated on human labels) that raises precision of the released set.
+4. **Type-indexed retrieval** over the verified set, tested as a downstream aid to provers.
+
+## 3. Brief
+
+### 3.1 Introduction (about 1 page)
+- Autoformalization of research-level and textbook mathematics is the bottleneck for formal libraries; existing benchmarks are competition problems or small curated sets.
+- Textbooks are the real input: PDFs with broken math fonts, items split over pages, definitions that depend on context.
+- Everyone reports compile rate. Compile rate cannot see a well-typed statement of the wrong theorem. We quantify that.
+- Preview of findings (to be filled with real numbers): gap size, which stage loses the most, what the filter recovers.
+- Contributions list as in section 2.
+
+### 3.2 Related work (about 0.75 page)
+Group into four threads. Entries are from memory and **must be verified and completed before submission**.
+- *Autoformalization benchmarks*: miniF2F, ProofNet (undergraduate textbook theorems, the closest prior), PutnamBench, FormalMATH, Lean Workbook, CombiBench. Gap we fill: page-grounded extraction from raw PDFs, human fidelity labels, definitions and exercises, not only theorem statements.
+- *Autoformalization models and training*: Wu et al. 2022 (few-shot with LLMs), Herald, Kimina-Autoformalizer, Goedel-Prover and DeepSeek-Prover family, repair with compiler feedback and type-check filtering (Poiroux et al. line of work). We use these as baselines, not competitors.
+- *Faithfulness / semantic equivalence checking*: FormalAlign, back-translation and LLM-judge approaches, ProofNet# style manual correction. We compare our filter against these.
+- *Document understanding for mathematics*: math OCR (Nougat, Mathpix-style systems), PDF-to-LaTeX pipelines, and statement mining from textbooks. We compare our vision-OCR route and anchor-based span resolution.
+- *Premise and library retrieval*: LeanDojo/ReProver, Lean search tools (Moogle, LeanSearch). We position type-index retrieval relative to embedding retrieval.
+
+### 3.3 Key strategy (about 1.5 pages)
+1. **Ground everything in the page.** Quote anchors, not model-counted offsets; per-item `source_hash`, span and `page_checksum`. This is what makes human audit and re-run cheap, and it is the methodological difference from ProofNet-style curation.
+2. **Separate four claims that today are conflated:** *detected* (an item exists at this span), *compiled* (Lean accepts), *proved* (no `sorry`), *faithful* (matches the source). The pipeline reports each separately. Fix the overloaded `unverified` label first, since "Lean rejected" and "Lean never ran" currently look identical.
+3. **Fidelity filter.** Informalize the Lean statement back to natural language with a model that never saw the source, then judge equivalence against the source span with a multi-model ensemble; calibrate thresholds against human labels. Report precision/recall of the filter against humans, not agreement among LLMs.
+4. **Make every stage ablatable.** OCR mode (text / auto / ocr), window size, repair attempts, model choice, each toggle changes one thing and gets measured.
+5. **Release without releasing the book.** Use openly licensed sources for the public set (see 4.1); for copyrighted books release only spans' hashes, Lean code and instructions to reproduce, never page text.
+
+### 3.4 Detailed experiments (about 2.5 pages)
+
+**E1. Benchmark construction and statistics.**
+Sources: at least 6-8 books across algebra, analysis, topology, number theory, combinatorics; at least 3 with an open licence. Report items per book, kinds, span lengths, cross-page rate, OCR failure rate. Target 1,500+ items, with a 600-item human-audited core.
+
+**E2. Detection quality.**
+Humans mark ground-truth items on 150 pages (stratified by book and by OCR difficulty). Report span precision, recall, boundary exact-match and IoU; breakdown for cross-page items. Ablate window size (1/2/3/5), extractor (text / auto / ocr), detection model. Report run-to-run variance over 5 repeats to address the 80-vs-89 instability.
+
+**E3. OCR / extraction.**
+On pages with known font damage, compare embedded text, tesseract, the vision model, and one dedicated math-OCR system on LaTeX token accuracy and on downstream item yield. Includes the auto-mode quality heuristic's accuracy against human judgement.
+
+**E4. Formalization: compile rate vs fidelity (the central experiment).**
+Models: at least four general LLMs (e.g. Qwen, one OpenAI, one Anthropic, one DeepSeek) plus at least one specialised autoformalizer. Metrics per model: compile rate, proved rate, human-judged fidelity, and the gap. Breakdown by item kind (definition / theorem / problem), domain, length, dependency on prior context. Report cost per verified-and-faithful item.
+
+**E5. Human annotation protocol.**
+Two Lean-literate annotators label each item {faithful, minor drift, wrong, wrong-but-compiles}; third resolves. Report Cohen's kappa; guideline and error taxonomy (missing hypothesis, wrong quantifier, vacuous statement, changed definition, over-general). Include a taxonomy figure; this is the analysis section reviewers will remember.
+
+**E6. Fidelity filter evaluation.**
+Compare: no filter, type-check only, single-LLM judge, judge ensemble, round-trip plus ensemble. Report precision/recall/F1 for "faithful" against the human core, and precision of the retained set at fixed recall. Include a negative control (shuffled spans) to show the filter is not rubber-stamping.
+
+**E7. Repair ablation.**
+Repair attempts 0/1/3/5. Key question: does repair improve fidelity or only compile rate? Expect compile rate up and fidelity flat or down; if so, that is a headline finding.
+
+**E8. Downstream use: type-indexed retrieval.**
+On held-out exercises, give a prover model (a) nothing, (b) embedding-retrieved items, (c) type-index retrieved items, from the verified-faithful set; report pass@k. Also run on faithful vs unfiltered store to show filtering matters downstream. Keep this modest: it supports a contribution, it does not carry the paper.
+
+**E9. Contamination check.**
+For each formalization model, test whether items exist verbatim in public Lean corpora (Mathlib docstrings, ProofNet); report results on the clean subset.
+
+**E10. Error analysis and cost.**
+Failure cases by pipeline stage, token cost, wall-clock per page, Lean time per item.
+
+### 3.5 More detailed experiments (second layer, if time allows)
+- **Scaling:** performance vs book length and vs number of dependencies on earlier chapters; a context-carrying variant that supplies earlier definitions.
+- **Cross-lingual / non-English books** (project has Chinese-language tooling already): detection and OCR on Chinese textbooks, for the ACL audience.
+- **Judge bias:** does the judge prefer outputs from its own family? Cross-family judging matrix.
+- **Human effort study:** time to audit with page-grounded span vs. without; supports the provenance design.
+- **Robustness to scan quality:** degrade page images (DPI, noise) and measure yield.
+- **Homogenization angle** (ACL 2027's optional theme): do models converge on the same wrong formalization? Measure agreement among wrong outputs across models.
+
+## 4. Work plan to the 4 Jan 2027 deadline
+
+### 4.1 Preconditions (week 1-2, 21 Oct - 3 Nov)
+- Fix the overloaded `unverified` label; add the `source_pages` coverage table; incremental per-item storage (all three already queued).
+- Choose the open-licence sources and confirm their licences (do not reuse the uiowa-algebra book for any released file).
+- Write annotation guideline; recruit two annotators; set up an annotation UI over the existing page-grounded provenance.
+- Freeze a pipeline version and a model list; log all prompts and model ids.
+
+### 4.2 Data and runs (weeks 3-6, 4 Nov - 1 Dec)
+- Ingest all books; produce the item pool; draw the 150-page detection sample and the 600-item core.
+- Run E2, E3, E4 for all models.
+
+### 4.3 Annotation and method (weeks 5-9, 18 Nov - 22 Dec)
+- Human labelling of the core; compute agreement.
+- Build and calibrate the fidelity filter; run E5-E7.
+- Go / no-go on 8 Dec: if the filter gives no clear gain over a single-LLM judge, submit as a pure evaluation-and-analysis paper and drop contribution 3.
+
+### 4.4 Downstream and writing (weeks 8-11, 9 Dec - 3 Jan)
+- Run E8-E10; write the paper in parallel from 1 Dec; internal review 24 Dec; release the licence-clean data and code package; ARR submission by 3 Jan to leave a day of slack.
+
+## 5. Risks and mitigations
+| Risk | Mitigation |
+|---|---|
+| Annotation too slow | Fix the audited core at 600; stratified sampling; second annotator on a 30% overlap only for kappa |
+| Fidelity filter shows no gain | Pure analysis paper; the gap measurement is the contribution |
+| Reviewers call it an engineering paper | Lead with the gap measurement and error taxonomy, not the pipeline |
+| Licensing blocks release | Open-licence books for the public split; hash-only releases for the rest |
+| Model API cost or drift | Pin model ids, cache outputs, report dates of calls |
+| Lean/Mathlib version drift | Pin the image (toolchain + Mathlib revision) per release |
+| Dates move | ICML and NeurIPS D&B dates are projected; re-check official CFPs before committing |
+
+## 6. Sources checked on 2026-10-21
+- ACL 2027 site (official): ARR deadline 4 Jan 2027, Kyoto 20-22 Aug 2027.
+- NAACL 2027 call: ARR deadline 12 Oct 2026 (closed).
+- ICLR 2027 call: paper deadline 25 Sep 2026 (closed).
+- CPP 2027 page: paper deadline 10 Sep 2026 (closed).
+- ITP 2027 site: Glasgow, early Aug 2027, deadlines not yet published.
+- OpenCurious / trybibby aggregators: ICML 2027, IJCAI 2027, COLM 2027, NeurIPS 2027 (projected, unofficial).