docs: add ACL 2027 bar analysis and link the research plan from the README

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6

README.md

@@ -265,6 +265,13 @@ it; re-run the workflow with `refresh_service=true` to move it onto the new imag
 | `REGISTRY_TOKEN` | secret | a personal access token with `write:package`. **The built-in Actions token is not accepted by Gitea's container registry**, so without this the image is not pushed — it is still built and kept on the runner, and the build does not fail |
 | `REGISTRY_USER` | variable | only if the pushing account is not the actor |
 
+## Research plan
+
+The paper plan for this project (ACL 2027 target, ARR deadline 4 Jan 2027) lives in
+[`docs/research-plan.md`](docs/research-plan.md), with the work list in
+[`docs/TODO.md`](docs/TODO.md) and the acceptance-bar analysis in
+[`docs/acl-2027-bar.md`](docs/acl-2027-bar.md).
+
 ## What this does not claim
 
 Lean says whether the code is *legal*, and — when there is a proof — whether it is

docs/acl-2027-bar.md

@@ -0,0 +1,43 @@
+# Reaching the ACL 2027 bar
+
+Companion to `research-plan.md` and `TODO.md`. Written 2026-10-21. Target: ACL 2027 via ACL Rolling Review (ARR), submission deadline **4 Jan 2027** (AoE), 8-page long paper.
+
+## What the bar is
+
+Based on ACL 2025 and the ARR review form (the 2027 form may differ; re-check when published).
+
+- ACL 2025 accepted 20.3% of committed papers to the main conference and 16.7% to Findings ([program chairs' report](https://www.aclweb.org/adminwiki/index.php/2025Q3_Reports:_Program_Chairs)).
+- The [ARR review form](https://aclrollingreview.org/reviewform) scores Soundness, Excitement, Reproducibility, Datasets (1-5) and Software (1-5), plus an overall score: 4 = could be accepted to the main conference, 3 = Findings (soundness and reproducibility are the main criteria), 2 = resubmit next cycle.
+- Reviewers write numbered weaknesses (concerns that would rank the paper below other strong submissions). Every likely weakness should already be answered on the page.
+
+So the goal is an overall score of about 4, with Findings as the realistic floor.
+
+## Where the paper stands against each score
+
+| Score | What gets a 4 | Where we are today | What closes it |
+|---|---|---|---|
+| Soundness | Claims supported by a calibrated evaluation with baselines, CIs and a human check | No results, one model, no human labels | E4-E6 with kappa on 200 overlapping items, 600 audited items, Wilson CIs, paired tests |
+| Excitement | A new idea, not a pipeline | Role-level structural fidelity + schema guidance, but 2026 papers already cover the gap and textbook pipelines | Show role alignment beats LLM judges on specific error types; say so in title and abstract |
+| Datasets | "Useful" or "Enabling" | Copyrighted book, 89 items | Open-licence split of 1,500+ items with simplex and fidelity labels |
+| Software | Usable release | Repo exists, no results | Pinned Docker image, one-command reproduction, tests |
+| Reproducibility | Mostly reproducible | Detection varies run to run (80 vs 89 items) | Fixed seeds, logged prompts, 5-repeat variance, pinned Lean and Mathlib |
+| Limitations / ethics | Honest and specific | Not written | Checklist in `research-plan.md` section 8.3 |
+
+## What must be true on 4 Jan
+
+1. **One headline result with a clean control.** At a fixed false-reject rate on faithful items, role alignment catches X% of "compiles but wrong" items versus Y% for a single LLM judge and Z% for a two-judge ensemble, with per-error-type recall. Everything else supports this.
+2. **Human labels you can defend.** Two annotators, kappa >= 0.6 on the overlap, blind to model and filter score. This is the item most likely to slip.
+3. **At least 4 models plus a specialised formalizer, and comparisons with existing metrics:** Beyond Compilation's judge rule, BEq+, static-pattern checkers, CriticLean. A 50-item ShadowBench-style check is enough.
+4. **Honest positioning.** Do not claim first textbook autoformalization or first gap measurement. Cite Beyond Compilation, ShadowBench, Lean-GAP and ATLAS on page one and say what they lack.
+5. **An error analysis reviewers remember:** a taxonomy of natural errors from real pages, a failure-case figure, and the repair finding (compile rate rises, faithfulness does not).
+6. **Released, licence-clean artifacts and an anonymized repository.**
+7. **A scope that fits 8 pages.** Cut the analogy miner, the Chinese-book study, the homogenization angle and the audit-time study (P2 in `TODO.md`). Keep schema-guided retrieval and proving (E9) only if the schedule holds.
+
+## Risk and fallbacks
+
+Eleven weeks is tight. The 8 Dec go/no-go decides the paper: if role alignment works, submit a method + resource paper aimed at the main conference; if it does not beat the baselines, submit an evaluation + resource paper aimed at Findings or the next cycle. Fallback venues: NeurIPS 2027 Datasets & Benchmarks (about May, projected), ITP 2027 (Glasgow, early Aug, dates pending), COLM 2027 (about 30 Mar, tentative).
+
+## Do now
+
+- Pilot the headline experiment on the existing 65 items with a quick manual label pass; if role alignment shows no signal there, find out before spending six weeks.
+- Check whether ARR requires every author to register as a reviewer for ACL 2027 (the NAACL 2027 call did); missing it can mean desk rejection.