lean-bench/docs/TODO.md

lean-bench paper TODO (target: ACL 2027 via ARR, deadline 4 Jan 2027 AoE; submit by 3 Jan)

Companion to docs/research-plan.md. Priorities: P0 blocks the paper, P1 needed for a strong submission, P2 only if time allows. Dates are targets. Updated 2026-10-21.

Working claim: a simplex schema derived from the Lean signature gives a cheap, structural, human-calibrated fidelity signal (role alignment) and guides formalization and retrieval; compiling alone overstates quality.

---

A. Next 7 days (21-28 Oct)

• P0 Read in full and take notes on the five closest papers: Beyond Compilation (2606.31002), ShadowBench (2608.29270), Lean-GAP (2606.02588), ATLAS (2605.29955), CriticLean (2507.06181). One page each: data, metric, numbers, what they do not do.
• P0 Decide the minimal simplex implementation: re-implement Role / Simplex / State inside leanbench/ (do not import the archived code). Write the design note.
• P0 Fix the overloaded unverified label -> rejected_by_lean vs lean_not_run (+ test).
• P0 source_pages coverage table (extractor, quality score, OCR ran/failed, timestamp) (+ test).
• P0 Incremental per-item storage so a crash keeps finished work (+ test).
• P0 Confirm licences for candidate open books (see C1). Shortlist 6-8.
• P1 Check Lean-GAP's Kaggle terms: can the human-signed statements be used as an external gold set?
• P1 Set up a weekly arXiv/Google Scholar alert for: autoformalization faithfulness; textbook Lean; semantic alignment Lean.
• P1 Ask the owner for two annotators (Lean-literate) and agree pay/time.

B. Code: simplex schema and alignment (weeks 1-4)

• P0 leanbench/schema.py: Role(name, context, choices, attrs), Simplex (validation inside __init__, >= 2 roles, nesting), Fact/Goal with lean_type. Avoid the archived defects (dead __post_init__, missing Role.__init__ call, absolute import).
• P0 Projection lean_code -> Simplex extending typeindex.py: explicit binders, instance binders attached to their object, hypothesis binders as Fact roles, conclusion as Goal role, binder_kind for quantifiers. Tests on >= 100 real signatures. Acceptance: >= 95% structural agreement with manual parse (E0).
• P0 Source-side extraction prose -> Simplex (one forced tool call, minItems: 2, search-first role reuse). Prompt versioned and hashed.
• P0 Alignment A(S_T, S_L): matching on name similarity, kind, type compatibility; outputs matched / missing / extra / conflicts + typed error list. Deterministic and unit-tested.
• P1 Role registry in SQLite with search_roles, find_by_roles, find_solvable; migrate from archived schema_registry.py with tests for nesting depth > 1.
• P1 Slot-constrained formalization mode (--mode slots): model fills binder strings per role, declaration assembled deterministically; slot-level repair from Lean diagnostics ranges.
• P1 Ablation switches in the CLI: window, extractor, repair attempts, slot mode, closed vs open choices, schema key wording variants.
• P2 Port AnalogySchemaMiner; run only after main results.
• P1 Pin Lean/Mathlib image; add lean-bench doctor check that logs toolchain + Mathlib revision into every run record.
• P1 Reproducibility: run record per ingest (model ids, prompts hash, seeds, image id) stored in the DB.

C. Data (weeks 1-6)

• P0 C1. Choose 6-8 books (algebra, analysis, topology, number theory, combinatorics; >= 3 openly licensed; one Chinese-language for 7.7). Record licence, URL, hash. Candidates already used by others: Lebl Basic Analysis, McKay Topology, Doty Abstract Algebra (LaTeX, open) [confirm licences]; keep uiowa-algebra.pdf out of every release.
• P0 Ingest all books (E1). Target >= 1,500 items. Record cost and time per page.
• P0 Draw stratified samples: 150 pages for detection gold (E2), 600 items for the audited core (E5), 150 items for gold source-side simplices.
• P0 Annotation tool: page crop + Lean code + both simplices side by side; blinded to model id and filter score; stores annotator id and time.
• P0 Annotation guideline v1 with 30 worked examples and the error taxonomy (5.2). Pilot 50 items, compute kappa, revise. Gate: pilot kappa >= 0.6.
• P1 Collect natural error examples (not synthetic) for the taxonomy figure.
• P1 Build the release package structure (hashes + spans + Lean + simplex annotations; no copyrighted text).

D. Experiments (weeks 3-10), in run order

• P0 E0 projection coverage (>= 95%).
• P0 E2 detection: P/R/F1, boundary IoU, cross-page, 5-repeat Jaccard; ablate window/extractor/model.
• P1 E3 OCR: embedded vs tesseract vs vision vs one math-OCR; auto heuristic ROC.
• P0 E4 compile vs faithful across >= 4 general LLMs + 1 specialised formalizer, same budget; paired McNemar; bootstrap CIs; stratify by length/kind/domain/context dependency.
• P0 E5 human labels on the 600 core; kappa on 200 overlap; third adjudicator.
• P0 E6 filter comparison: no filter, type-check, single judge, two-judge, BEq+, static checkers, CriticLean/FormalAlign, trajectory length, role alignment, role alignment + judge. Metrics: P/R/F1, AUC, recall of wrong-but-compiles at 10% false-reject, per-error-type recall. Controls: shuffled spans, same-family judge.
• P0 E7 slot-constrained vs free-form (same model, same budget).
• P0 E8 repair ablation 0/1/3/5, whole vs slot-level; fraction of newly compiling items that are faithful.
• P1 E9 retrieval/guidance: no retrieval, BM25, embedding, LeanSearch v2, structure-aware retriever baseline (2510.23637-style), type index, find_solvable, oracle; 2 open provers + 1 API; pass@1 / pass@8.
• P1 E10 contamination check.
• P1 E11 cost/time/reliability table, including the silent-failure checks.
• P1 External check on Lean-GAP gold (if licence allows) and a spot check on ATLAS outputs.
• P2 7.1 role vocabulary growth/dedup; 7.2 dependency graph; 7.3 analogy mining; 7.4 judge-bias matrix; 7.5 robustness; 7.7 Chinese book + homogenization; 7.8 audit-time study.
• P0 Go/no-go on 8 Dec: if role alignment does not beat a single judge on at least two error types at equal false-reject, drop contribution C2 as a headline and submit as evaluation + taxonomy + provenance.
• P0 Freeze all tables on 24 Dec.

E. Writing (start 1 Dec; related work and method now)

• P0 Related-work section from the notes in research-plan.md section 4 (all [verify] tags cleared).
• P0 Method section: definitions (5.1), taxonomy (5.2), slot decoding (5.3), alignment (5.4), retrieval (5.5).
• P0 Introduction (draft exists in section 3); rewrite after E4 numbers.
• P0 Figures: F1 overview (page crop + two simplices), F2 gap by model, F3 error taxonomy, F4 ROC/recall at fixed false-reject, F5 retrieval/guidance.
• P0 Tables: T1 stats, T2 gap, T3 filter comparison, T4 ablations.
• P0 Limitations (LLM dependence of source-side extraction, one proof assistant, few books, annotator expertise, judges proprietary).
• P0 Responsible NLP checklist, data statement, annotator pay and instructions, licence statement.
• P1 Anonymized repository + artifact package; remove identity from images, paths, commits.
• P1 Internal read-through by someone outside the project, 24-27 Dec.
• P0 Format on ACL template, 8 pages; submit to ARR by 3 Jan 2027.

F. Risks to watch (check weekly)

• New arXiv papers overlapping role-level or structural fidelity checks. If one appears: read within 24 h, update the positioning table, decide whether C2 still stands.
• ICML 2027 / NeurIPS D&B 2027 official CFPs (dates are projected today).
• ITP 2027 CFP (Glasgow, ~2-7 Aug 2027) as fallback.
• Annotator availability; Lean compute (second runner if E4/E7/E8 exceed ~100 CPU-hours).
• API cost against the 135M-token estimate (recompute after pilot).

G. Milestones

Date	Milestone
3 Nov	Items in A and B-core done; E0 passes; books chosen
17 Nov	All books ingested; annotation pilot kappa >= 0.6
1 Dec	E2, E3, E4 finished; core labelling under way; writing starts
8 Dec	Go/no-go on role alignment
15 Dec	E5-E8 finished
24 Dec	Tables frozen; E9-E11 finished; full draft
27 Dec	Internal read-through done
3 Jan 2027	Submit to ARR (deadline 4 Jan AoE)