lean-bench/docs/research-plan.md

lean-bench: research plan and detailed paper brief (v2)

Written 2026-10-21. Version 2 replaces the first brief. Two changes: (1) the simplex schema (archived/schema-simplex) is now the central method, as requested; (2) every section is expanded to the level of draft text, protocols and metrics.

Evidence base: repo README and code (leanbench/, 4,345 lines incl. tests), project notes lean-bench-rebuild.md, runs/p85-110/*, the archived simplex code, and literature checked on 2026-10-21. Anything marked [verify] is from memory or an aggregator and must be checked before it goes in a submission.

---

0. The idea in one page

Simplex, as it exists in the archived code.

• Role(name, context, choices): a named semantic slot with a description and an optional closed set of allowed values (is_constrained, validate_value).
• Simplex(name, roles: {alias: Role}): a reusable unit of at least two roles. A Simplex is itself a Role, so simplices nest; nesting gives a simplicial complex. Equivalence is the two-role special case.
• State / Fact / Goal: a role plus a value. A Fact has a value, a Goal does not; SolvingTask.is_completed() is "every goal resolved".
• SchemaRegistry (SQLite): set_role, set_simplex, search_roles, find_by_roles(known_roles), find_solvable(known_role_names).
• SchemaParserAgent: turns a query into a Simplex through a forced tool call whose JSON schema says minItems: 2, with a search-first, reuse-before-create rule for roles. AnalogySchemaMiner: proposes new simplices by the ratio Simplex B : Role B :: Simplex A : Role A.

Why it is "exactly the Lean parameters". A Lean declaration is a simplex:

Lean	Simplex view
(G : Type*) [Group G]	role G, context = "carrier", choices = admissible type/class constraints
(h : P x) hypothesis	Fact role
conclusion after the final :	Goal role
def / structure being introduced	own role (what the thing is)
a lemma used inside a proof	nested simplex (edge in the complex)

leanbench/typeindex.py already extracts exactly this split: input (binders and hypotheses), goal (the conclusion), own (definitions). So the type index is a simplex index in all but name. The new work is to make it a first-class schema that steers inference instead of a passive index.

Four uses of the schema to guide inference (each is a testable claim):

1. Slot-constrained formalization. Decode a Lean declaration as filling a pre-declared simplex (typed slots, closed choice sets), the way register_simplex_schema forces minItems: 2 and role reuse.
2. Role-alignment fidelity check. Extract a source-side simplex from the prose (what is given, what is claimed) and compare it role by role with the Lean-side simplex. Missing hypothesis, extra hypothesis, wrong quantifier and swapped goal show up as role mismatches. This is a structural check that Lean cannot do and that does not rely on another LLM's opinion.
3. Schema-guided retrieval. find_solvable(known_roles): given the facts at hand, return items whose input roles are all covered and whose goal role matches. Compare with embedding retrieval.
4. Schema-guided proof search. Treat the proof task as SolvingTask(facts, goals); expand by applying a solvable simplex, adding its goal to the facts. Provers are steered by the registry rather than a flat premise list.

Paper claim (working): Lean acceptance overstates autoformalization quality; a simplex schema derived from the Lean signature gives a cheap, structural, human-auditable fidelity signal and a retrieval/guidance structure that improves both the faithfulness of the released data and downstream proving.

Working title: Parameters as Schema: Simplex-Guided Autoformalization of Textbook Mathematics, and Why Compiling Is Not Enough

Honest state of the evidence today

• Pipeline: runs end to end. The pages 85-110 run: 89 detected (48 statements, 41 problems), 65 formalized, 24 skipped, 10 verified, 1 proved (so compile rate on formalized items is 15%, and 85% of items fail or were not checked, with unverified conflating "Lean rejected" and "Lean never ran").
• Detection is not reproducible (80 vs 89 items on the same range).
• Faithfulness has never been measured. One book, one model.
• The simplex code is archived, not integrated, and has defects (section 5.7).
• The source book is copyrighted.

---

1. Venue decision (checked 2026-10-21)

Venue	Deadline	Status	Fit
ACL 2027 via ACL Rolling Review, Kyoto, 20-22 Aug 2027	ARR 4 Jan 2027, 8 pages long	Official (2027.aclweb.org); commitment/notification TBA	Primary. Resource + evaluation + method
ICML 2027	~16 Jan abstract / ~22 Jan paper	[verify] projected from 2026 cycle; CFP not out	Backup if E6/E9 show a clear method win
IJCAI 2027	~4 / 11 Jan	[verify] projected	Not recommended
ITP 2027, Glasgow, ~2-7 Aug 2027	not yet published	CFP pending	Good fallback for the Lean-correctness angle
COLM 2027	~30 Mar 2027	tentative	Fallback
NeurIPS 2027 Datasets & Benchmarks	~May 2027	projected	Fallback with more time
Closed	ICLR 2027 (25 Sep), CPP 2027 (10 Sep), NAACL/COLING 2027 ARR cycle (12 Oct), AAAI-27, NeurIPS 2026

What the ACL bar demands, mapped to this plan

Reviewer expectation	Where the plan meets it
Contribution beyond engineering	Role-alignment fidelity signal and schema-guided inference (sections 5, 6: E6, E7, E9)
Strong baselines and several models	E4/E6/E7 run >= 4 general LLMs + 1 specialised autoformalizer, and compare with 4 existing faithfulness methods
Human evaluation with agreement	E5: two annotators, kappa, 600-item core
Statistical rigor	Section 7.6: CIs, paired tests, multiple seeds
Released artefacts, licence-clean	Section 5.6 and 8: open-licence books public, hashes-only for copyrighted ones
Limitations, Responsible NLP checklist, reproducibility	Section 8.3 checklist
Fits 8 pages	Section 3-6 are written to map to a page budget (3.6)

---

2. Contributions and hypotheses

Contributions

• C1. A schema view of Lean declarations: Role / Simplex / nested complex, with a deterministic projection Lean signature -> simplex (extends typeindex.py), registry with reuse-before-create role governance.
• C2. Role-alignment fidelity check: source-side vs Lean-side simplex comparison, with a typed error taxonomy that falls out of role mismatches.
• C3. lean-bench: page-grounded textbook items with Lean code, simplex annotation and human fidelity labels on a 600-item core.
• C4. Empirical study of the compile-vs-faithful gap by model, item kind, domain and pipeline stage; and of schema-guided inference vs unguided.

Pre-registered hypotheses (state them before running; report them whether they hold or not)

• H1. Compile rate overstates human-judged fidelity by >= 15 points for every model tested, and the gap is larger for tool/feedback-augmented pipelines.
• H2. Repair with compiler feedback raises compile rate more than it raises fidelity (gap widens with attempts).
• H3. Role-alignment detects >= 70% of human-labelled "wrong but compiles" items at <= 15% false-reject on faithful items, and beats a single LLM judge at equal false-reject rate on missing-hypothesis and quantifier errors. (Threshold is a target, not a result.)
• H4. Slot-constrained formalization raises fidelity by >= 5 points over free-form generation with the same model and budget, mainly by reducing missing-hypothesis errors.
• H5. Schema-guided retrieval (find_solvable) improves prover pass@k over embedding retrieval on exercises that depend on earlier definitions.

---

3. Introduction: draft text and structure

3.1 Paragraph plan

1. Hook. Formal libraries grow slowly because turning human mathematics into Lean is expensive; textbooks hold most of undergraduate and graduate mathematics, and LLMs now translate statements fluently.
2. The measurement problem. Systems and benchmarks are scored by whether Lean accepts the output. But Lean checks types, not meaning: a statement missing a hypothesis, with ∃ for ∀, or over ℕ instead of ℤ compiles and is wrong. Concurrent work already shows large gaps on curated statement sets (Beyond Compilation: up to 29.5 points; ShadowBench: 61.8% compile vs 11.2% SA-Pass), and textbook pipelines report faithfulness only through uncalibrated LLM scores (ATLAS, Lean-GAP). What is missing is a cheap, structural check that says which parameter is wrong, calibrated against humans, on pages where extraction error compounds with formalization error.
3. Why textbooks are harder. Font-mangled PDFs (D for =, C for +), items split across pages, definitions that depend on context. Each stage can break meaning silently: in our own pipeline the first server run reported success while storing 0 items.
4. Our observation. A Lean declaration's parameters are a small typed schema: given objects, hypotheses, a goal. The same schema exists in the prose (what is assumed, what is claimed). Comparing the two role by role is a structural check that localizes the error.
5. Approach. Represent both sides as simplices; use the schema to constrain formalization, to compare, and to retrieve.
6. Findings (fill in). "On N items from K books, M models compile X-Y% but only A-B% are faithful (gap G points). Role alignment recovers P% of unfaithful-but-compiling items at Q% false rejection; slot-constrained decoding raises fidelity by R points; schema retrieval raises prover pass@8 from S to T."
7. Contributions (C1-C4).

3.2 Opening paragraph (draft, to be edited)

Formalizing mathematics in a proof assistant remains slow because every definition and statement must be rewritten by hand. Large language models now produce plausible Lean 4 for textbook statements, and benchmarks report the share that the Lean compiler accepts. That number is easy to compute and easy to misread: Lean verifies that a statement is well typed, not that it says what the author wrote. A statement that drops a hypothesis, swaps a quantifier, or silently changes the ambient number system compiles and is wrong. We ask how large this gap is on real textbook pages, where extraction errors from the PDF compound errors from the model, and whether the structure of a Lean declaration itself can be used to detect and reduce it.

3.3 Figure 1 (spec)

Left: a PDF page crop (Definition + Proposition). Middle: source-side simplex (roles: G: finite group, n = |G|, g: element; goal: g^n = e). Right: Lean-side simplex from theorem ... (G : Type*) [Group G] [Fintype G] (g : G) : g ^ Fintype.card G = 1. Colored links per role; one red unmatched role in a failing example (the missing [Finite G] or an ℕ-for-ℤ slip). Caption states compile = yes, faithful = no.

3.4 Claims to avoid (reviewer traps)

• Do not claim "verified" means correct; use compiled, proved, faithful as four separate words from the first page.
• Do not claim novelty of the idea that compile != faithful (prior work shows it). Novelty is the structural role-level signal, the textbook-scale pipeline with provenance, and the guided inference.
• Do not claim the benchmark is large; say what it is (hundreds of audited items from a handful of books) and why.

3.5 Preview results table (to fill)

Model	compile %	proved %	faithful % (human)	gap (pts)	faithful after role filter %

3.6 Page budget (8 pages, ACL long)

Intro 1.0 | Related 0.6 | Method (simplex, alignment, guidance) 1.8 | Benchmark + protocol 1.0 | Experiments 2.6 | Analysis + conclusion 0.5 | Limitations and ethics on extra pages. Figures: F1 overview, F2 gap by model, F3 error taxonomy, F4 role-alignment ROC, F5 retrieval/guidance. Tables: T1 stats, T2 gap, T3 filter comparison, T4 ablations.

---

4. Related work: threads, references, and the sentence that separates us

References marked [verify] are from memory/search snippets; confirm authors, year and numbers before citing.

4.1 Autoformalization benchmarks and corpora

• miniF2F, PutnamBench, FormalMATH, CombiBench, Lean Workbook: competition-style or synthetic. [verify each]
• ProofNet (Azerbayev et al., 2023; undergraduate textbook theorems; arXiv 2302.12433): closest prior. Hand-curated, statements only, no extraction from PDFs.
• ProofNet#, RLM25, ProofNetVerif (Poiroux et al., arXiv 2406.07222): fixed 118 of 371 ProofNet entries; found type-check rate correlates only weakly (Pearson 0.655) with human accuracy; proposed BEq/BEq+ symbolic equivalence (BEq+ precision 98.0%, recall 48.3%).
• Beyond Compilation (arXiv 2606.31002, read in full 2026-10-21). 227 graduate statements taken from four open LaTeX textbooks (Lebl Basic Analysis 48, Lebl Complex Analysis 19, McKay Topology 63, Doty Abstract Algebra 97). Faithful = compiles AND both judges (GPT-5.2, Gemini-2.5-Pro) grade >= 9/10. Human audit: positive precision 67/70 = 95.7%; of 67 compile-pass outputs the rule rejected, humans confirmed 54 (80.6%); a 59-case Aristotle batch gave 91.5% agreement. Beats LeanScorer (76.3% vs 91.5% on that batch; McNemar p = 0.0225). BEq cross-check certified 116/189 pairs (61.4%). Eight systems: full tool-augmented GPT-5.2 agent compiles 87.2% but is faithful on 57.7% (gap 29.5); one-shot general LLMs faithful 19.8-27.3%; specialised formalizers 10.1-13.8%; prover-oriented 4.6-6.2%. Ablation: Lean feedback adds +49.3 compile but +22.1 of that is unfaithful; faithfulness falls from 82.9% (1-2 agent steps) to 11.5% (19-24 steps). Stated limits: proprietary judges, same-family orchestrator, 227 items, no kappa reported in the visible text. Code/data: github.com/grenadeComing/beyond-compilation.
• ShadowBench / SA-Pass (arXiv 2608.29270, read 2026-10-21). 178 postgraduate/research problems from textbooks, notes, papers, Mathlib, Stacks, EGA. A shadow is a theorem implied by the intended statement; a candidate must compile, imply every shadow and be implied by their conjunction. Shadows are drafted by Qwen3-235B and completed by experts (706 checkers, ~10 min per problem, hidden from submitters). Best system (Claude Code Opus 4.8 + Numina) compile 61.8% vs SA-Pass 11.2%; non-agentic LLMs 0.0% SA-Pass. Agreement with two experts: SA-Pass 0.988, BEq+ 0.806, LLM-judge 0.785, compile 0.178. On ProofNet the gap is only 2.1 points on average, which the authors attribute to short single-conclusion targets. Cost of the method: per-problem shadow authoring.
• Lean-GAP (arXiv 2606.02588). Closest to our pipeline. 430 of 1,966 Dummit & Foote Abstract Algebra exercises: scanned pages -> Mathpix OCR -> LLM -> Lean sorry statements, human contributors, two-stage human sign-off, 11 "suspicious-statement" static patterns (C1-C11), Claude Opus 4.7 five-axis judge (uncalibrated). Six systems; GPT-5 elaborates 44.1% and is judged faithful 45.1%; Codex agent elaborates 95.5% but faithful 51.2%. Released on Kaggle with Wiley's permission for non-commercial research [confirm terms].
• ATLAS / AutoformBot (arXiv 2605.29955). 26 open-access graduate textbooks, > 45,000 Lean declarations, ~500k lines, 71.3% formalization rate; faithfulness only through an LLM 0-5 harness (threshold 3/5). No human calibration reported in the summary I read. 26 separate projects, not Mathlib-compatible.
• LeanFlow (arXiv 2607.20503): paper -> Lean workflow with a blueprint mapping source spans to declarations and an LLM statement-review gate; states that "no automated faithfulness check exists". Two papers only.
• Faults in Our Formal Benchmarking (arXiv 2606.29493): audits miniF2F, ProofNet, FormalMath, CombiBench, ProverBench (~10,000 problems), 4,833 findings, 398 with machine-checkable certificates; fidelity defects include missing hypotheses, vacuous hypotheses, ℕ subtraction truncation, division by zero. Its checkers are cheap static baselines for us.
• How we differ, stated carefully. Textbook-to-Lean pipelines (Lean-GAP, ATLAS, LeanFlow) and faithfulness measurement (Beyond Compilation, ShadowBench) both exist. What none of them does: (a) a structural, role-level fidelity check that localizes which parameter is wrong and needs no per-item authoring (shadows) and no extra judge call; (b) calibrating that check against humans at the role level; (c) page-level provenance with a coverage record so extraction and formalization errors are separable; (d) schema-guided generation and retrieval built from the same roles. The paper must not be sold as "first textbook autoformalization".

4.2 Autoformalization methods

• Few-shot autoformalization (Wu et al., 2022 [verify]); sampling + type-check filtering + selection (2406.07222); Herald, Kimina-Autoformalizer, Goedel-Prover, DeepSeek-Prover-V2 [verify each]; agentic Lean workflows (e.g. Numina-Lean-Agent as used in ShadowBench [verify]).
• How we differ: we do not propose another model. We propose a schema layer that constrains and audits any model, and treat these systems as baselines.

4.3 Faithfulness and equivalence checking

• FormalAlign (Lu et al., ICLR 2025; arXiv 2410.10135): Mistral-7B fine-tuned with cross-entropy + contrastive loss; score = mean of certainty and cosine similarity, threshold 0.7; trained on synthetic misalignments (~21 negatives per positive); trails GPT-4 on FormL4-Random and MiniF2F-Test; human study of 80 items with Fleiss kappa 0.49. Lesson for us: synthetic negatives do not match real errors, so evaluate on naturally occurring errors from textbook pages.
• BEq / BEq+ (Poiroux et al.): symbolic, precision 98.0%, recall 48.3%. TransTED / ASSESS (arXiv 2509.22246; 1,247 expert-annotated pairs; accuracy 67-70%; ~51 s per pair; threshold varies 0.38-0.61 by benchmark; false positives on near-misses).
• CriticLean (arXiv 2507.06181): trained critic for faithfulness; CriticLeanBench 500 pairs; Qwen3-32B-RL 87.0% vs Gemini 2.5 Pro 89.2%; critic raised Kimina-Autoformalizer-7B from 54% (compiler feedback) to 84% on a 50-problem human check; ~47% of problems still failed in 200 attempts.
• LLM-judge ensembles (Beyond Compilation) and shadow statements (ShadowBench): behavioural checks that need extra LLM calls or authored shadows (~10 min per item).
• Static fidelity checkers: Lean-GAP's C1-C11 patterns and the checkers of Faults in Our Formal Benchmarking.
• Back-translation / round-trip consistency: used inside several of the above; [locate a specific citation before claiming it].
• How we differ: role alignment is structural and gives a typed explanation of which part of the statement is wrong. It is cheap (one extraction call + deterministic matching), and complements, not replaces, BEq and judges. We evaluate all of them side by side (E6).

4.4 Structured / schema-guided reasoning with LLMs

• Schema-constrained decoding and JSON-schema tool calls; type-directed / grammar-constrained generation [verify specific papers]; frame semantics and semantic-role labelling as the linguistic precedent for "roles"; analogical structure mapping (Gentner) as precedent for the analogy miner.
• Found 2026-10-21 (titles from search results; read them and confirm claims before citing): "Schema Key Wording as an Instruction Channel in Structured Generation under Constrained Decoding" (arXiv 2604.14862), which suggests the wording of schema keys itself steers the model, so role name/context strings are a design variable to ablate in E7; "Constrained Decoding Eliminates Structural Failures in Small LLMs but Reveals a Scale-Dependent Semantic Gap" (arXiv 2609.23742), the same structure-is-not-semantics lesson as compile-is-not-faithful, and a useful motivation for pairing slot constraints with role alignment; SLOT (arXiv 2505.04016) and an empirical study of structured-output control (arXiv 2606.09395).
• How we differ: roles come from the Lean signature itself, so schema and ground-truth parameters coincide; the registry reuses roles across the whole corpus. Our constraint is on what the declaration is about (its parameters), not only on output syntax.

4.5 Mathematical document understanding

• Math OCR and PDF-to-LaTeX (Nougat and commercial systems [verify]), vision LLM transcription; statement mining from LaTeX sources (arXiv-based corpora [verify]).
• How we differ: we handle the font-encoding failure mode specifically (ASCII look-alikes) and tie each OCR page to downstream item yield.

4.6 Premise selection and library search

• LeanDojo / ReProver, Lean search engines (Moogle, LeanSearch) [verify]; type-based search (Hoogle-like).
• Found 2026-10-21 (confirm before citing): LeanSearch v2, global premise retrieval for Lean 4 (arXiv 2605.13137); LeanExplore (arXiv 2506.11085); "Premise Selection for a Lean Hammer" (arXiv 2506.07477); "Combining Textual and Structural Information for Premise Selection in Lean" (arXiv 2510.23637), the closest to a structure-aware retriever and a required baseline in E9. These are text/embedding/graph retrievers over Mathlib; none indexes by the hypothesis/goal role signature of items extracted from textbooks.
• How we differ: find_solvable retrieves by role coverage across a corpus we built from textbooks, including items that are definitions and exercises, not only Mathlib lemmas.

4.7 Positioning table (include in paper)

Work	Input	Fidelity signal	Cost	Localizes error?	Textbook PDFs
ProofNet(#)	curated	human	high	n/a	no
BEq+	statement pairs	symbolic	CPU	no	no
TransTED / ASSESS	statement pairs	tree edit + tactics	~51 s/pair	no	no
LLM judges (Beyond Compilation)	LaTeX textbook statements	2-judge agreement	2 calls	no (text rationale)	LaTeX, not PDF
ShadowBench	curated	shadows	~10 min authoring/item	partly	no
Lean-GAP	scanned pages (Mathpix)	human sign-off + uncalibrated LLM judge	high human cost	no	yes, exercises only
ATLAS	26 open textbooks	uncalibrated LLM 0-5	calls	no	yes, no human calibration
Ours	PDF pages	role alignment (+ judges)	1 call + CPU	yes, by role	yes

---

5. Key strategy

5.1 Formal setup

• A source item is a span s = (hash, page_a:i_a -> page_b:i_b) with text t(s).
• A Lean item is code c with signature parsed into binder groups.
• Lean-side simplex S_L(c): deterministic projection (extend typeindex._split_top_level / _top_level_result):
  • one role per explicit binder (x : T); choices = {T} plus instance binders [C T] attached to the same role;
  • one Fact role per hypothesis binder whose type is a Prop; one Goal role for the conclusion;
  • own role for definitions.
  • Requirement: at least two roles; items with fewer (e.g. a bare def) are stored as degenerate and reported separately.
• Source-side simplex S_T(s): produced by one LLM call on t(s) only (never sees the Lean), as a forced tool call whose JSON schema has minItems: 2, fields alias, name, context, choices, kind in {object, fact, goal}; role names are resolved against the registry with search-first reuse.
• Alignment A(S_T, S_L): a bipartite matching on roles by (a) name similarity via registry, (b) kind, (c) type-compatibility of choices. Output: matched pairs, unmatched source roles (missing in Lean), unmatched Lean roles (extra in Lean), type conflicts, kind conflicts. Score = F1 over roles, plus a typed error list.

5.2 Error taxonomy derived from alignment

Role-level signature	Error type
source Fact unmatched	missing hypothesis
Lean Fact unmatched	extra hypothesis
matched object, choices differ	wrong type / wrong ambient structure (ℕ vs ℤ, Group vs CommGroup)
goal matched, quantifier prefix differs	quantifier error (detected on the goal role's quantifier annotation)
Lean has fewer than two roles	vacuous / degenerate statement
goal unmatched	wrong conclusion
Quantifier structure is not a pure role property; record it as a role attribute (binder_kind) extracted on both sides.

5.3 Slot-constrained formalization (guided inference, use 1)

Procedure per item:

1. Build S_T from the prose (above).
2. Ask the model to emit Lean as slot fills: for each role, a Lean binder string, with choices restricted to the role's choices when set (e.g. instance classes from a closed Mathlib list), and the goal as a separate field. The final declaration is assembled deterministically, so the signature always has the role structure.
3. Lean check; on error, repair only the offending slot (diagnostics map to character ranges, ranges map to slots), not the whole declaration. Ablations: free-form vs slot-filled; slot repair vs whole-declaration repair; open vs closed choices.

5.4 Role-alignment filter (use 2)

• Compute A(S_T, S_L) for every compiled item; accept if score >= tau and no hard error (missing hypothesis, kind conflict). tau calibrated on the 600-item human core to fix false-reject rate.
• Combined filter: role alignment AND (round-trip judge, optional). Evaluate each alone and combined.

5.5 Schema-guided retrieval and proof guidance (uses 3 and 4)

• find_solvable(known_roles): returns items whose input roles are covered by the given facts. Rank by goal-role match then by coverage tightness.
• Proof guidance: SolvingTask(facts, goals); at each step the prover is shown the top-k solvable simplices (with Lean statements) and may apply one; the applied simplex's goal becomes a new Fact. Stops when all goals are resolved or the budget ends. This is a thin loop around any prover; the contribution is the retrieval structure.
• Nested simplices record which items use which definitions; this is the dependency graph of the book.

5.6 Role vocabulary governance and release policy

• Reuse before create (from SchemaParserAgent): the agent must call search_roles on extracted keywords and reuse exact names. Metric: role-vocabulary growth per 100 items and duplicate-role rate (E-S2).
• Analogy mining (from AnalogySchemaMiner): propose new simplices from Simplex A : Role A :: Simplex B : Role B; quality-controlled by refusal when the analogy is weak. Evaluate in section 7 only; it is not on the critical path.
• Release policy: public split = openly licensed books (confirm licence per book); for copyrighted books release hashes, spans, Lean code and simplex annotations, never page text or OCR text. uiowa-algebra.pdf stays out of every release.

5.7 Porting work required (the archived code is not drop-in)

Found by reading archived/schema-simplex on 2026-10-21:

• Simplex is a @dataclass that defines its own __init__; the generated __init__ is therefore not used and __post_init__ never runs, so the "at least two roles" check never fires. Same for Equivalence ("exactly 2"). Move validation into __init__.
• Simplex.__init__ does not call Role.__init__, so context and _choices are never set; is_constrained() on a Simplex raises AttributeError.
• schema_builder.py imports from role import Role (absolute) alongside package-relative imports; will not import as a package.
• State/Fact/Goal carry a value but no Lean type; add lean_type.
• schema_registry.py has find_by_roles and find_solvable, but how nested simplices are stored and queried (keys("schema:*")) needs a test for depth > 1.
• Add: Lean signature -> simplex projection, role attributes (binder_kind, instance_of), alignment function, and unit tests in the style of the existing 12 test modules.

5.8 Separation of claims (carried from v1)

Report four independent flags per item: detected, compiled, proved, faithful (human, then filter). Split the overloaded unverified into rejected_by_lean and lean_not_run. Add the queued source_pages coverage table and incremental storage first, so every statistic can be recomputed.

---

6. Detailed experiments

Common protocol: Lean/Mathlib image pinned (Lean 4.33.1 image from the project); every model call logged with model id, date, temperature, prompt hash; 3 seeds where sampling is involved; items keyed by sha1(source hash + span) so runs are comparable; human labels stored with annotator id.

E0. Port and unit-validate the simplex projection (week 1-2)

• Question: does the deterministic Lean -> simplex projection cover the corpus?
• Data: the 65 existing items plus 300 items from other books.
• Metrics: % items with >= 2 roles; % hypotheses recovered vs manual count on 100 items; failure classes (tactic-block binders, variable inheritance, implicit universes).
• Pass bar: >= 95% structural agreement with manual parse; otherwise fix before any other experiment.

E1. Corpus and benchmark construction

• Sources: 6-8 books across algebra, analysis, topology, number theory, combinatorics, at least 3 openly licensed [confirm licences], one non-English (Chinese) for the second-layer study.
• Targets: >= 1,500 items; 600-item stratified audited core (by book, kind, page range, OCR status).
• Report: items per book/kind, items per page, span length, cross-page rate, truncated rate, OCR replaced/failed pages, roles per item, role vocabulary size.
• Reference point: 89 items over 26 pages = 3.4/page, projecting about 2,000 for the 587-page book.

E2. Detection quality

• Setup: two annotators mark every item on 150 stratified pages (50 per difficulty tier: clean text / mild damage / heavy damage).
• Systems: current detector with window 1/2/3/5; extractor text/auto/ocr; 3 detector models; baseline regex on "Theorem/Lemma/Definition/Exercise" headers.
• Metrics: span precision, recall, F1; exact-boundary match; token-IoU; cross-page recall; unresolved-anchor rate; run-to-run Jaccard over 5 repeats (to quantify the 80 vs 89 instability).
• Analysis: error classes (merged items, split items, missed exercises (a)/(b) sub-items, hallucinated spans).

E3. Extraction / OCR

• Systems: embedded text; tesseract; qwen-vl-max at 150/200/300 dpi; one dedicated math-OCR system [choose].
• Metrics: LaTeX token edit distance on 100 hand-corrected pages; formula-level exact match; downstream item yield and compile rate; cost per page; accuracy of the auto quality heuristic (threshold 0.75) vs human "page is damaged" judgement (ROC).
• Check: the ASCII look-alike failure (D for =, C for +) as its own error class.

E4. Compile vs faithful gap (central measurement)

• Systems: >= 4 general LLMs (one each from Qwen, OpenAI, Anthropic, DeepSeek families) + 1 specialised autoformalizer, same prompt and repair budget; same 600-item core.
• Metrics per system: compiled %, proved %, faithful % (human), gap = compiled - faithful; cost (tokens, USD) per faithful item; Lean time per item.
• Breakdowns: statement vs definition vs problem; algebra vs analysis etc.; short vs long; dependency on earlier context (needs earlier definition) yes/no.
• Test: paired McNemar between systems; bootstrap CIs for gap.
• Tests H1.

E5. Human annotation protocol

• Label set: faithful / minor drift / wrong-but-compiles / does-not-compile / not-formalizable.
• Procedure: two Lean-literate annotators label all 600; third adjudicates disagreements; 200-item overlap for kappa; guideline with 30 worked examples; annotators see the source page crop and the Lean code, not model identity or filter scores.
• Report: Cohen's kappa overall and per class; confusion matrix; annotation time per item (supports the provenance design).
• Also annotate: the error type from the taxonomy in 5.2, and the gold source-side simplex for 150 items (to evaluate extraction of S_T separately).

E6. Role-alignment fidelity filter (main method)

• Systems compared on the same core:
  1. no filter (compile only)
  2. type-check only
  3. single LLM judge
  4. two-judge agreement (as in Beyond Compilation [verify])
  5. BEq+ against a reference formalization, where one exists (ProofNet-style subset)
  6. shadow-style check on 50 hand-built items (small, illustrative)
  7. role alignment (ours)
  8. role alignment + judge
  9. static suspicious-pattern checkers (Lean-GAP C1-C11 style; Faults-in-Formal-Benchmarking style): cheap baseline that catches vacuity and ℕ-subtraction hazards
  10. a trained critic (CriticLean released model, if weights are available) and FormalAlign
  11. agent-trajectory-length signal (Beyond Compilation found faithfulness collapses with many repair steps): a free baseline from our own repair logs
• External gold set (saves annotation): if the Lean-GAP release permits, score role alignment against its human-signed exercise statements and its model outputs; if the terms forbid redistribution, use it only locally for evaluation and report aggregate numbers. [confirm Kaggle terms]
• Metrics: precision, recall, F1 for "faithful"; ROC-AUC for alignment score; recall of "wrong-but-compiles" at fixed false-reject 10%; per-error-type recall (missing hypothesis, extra hypothesis, type, quantifier, goal); cost per item (calls, CPU).
• Controls: shuffled spans (alignment must fail), identity (Lean vs its own back-translation), and judge self-preference (judge from same family as generator vs different).
• Quality of S_T itself: role precision/recall of source-side extraction against the 150 gold simplices; sensitivity to extractor model.
• Tests H3.

E7. Slot-constrained vs free-form formalization

• Design: same model, same budget, three arms: free-form; slot-filled with open choices; slot-filled with closed choices (instance classes from a Mathlib list).
• Metrics: compiled %, faithful % (human on the core, filter elsewhere), error-type distribution, tokens per success.
• Controls: matched number of Lean calls.
• Tests H4.

E8. Repair ablation

• Design: repair attempts 0/1/3/5; whole-declaration vs slot-level repair.
• Metrics: compiled %, faithful %, and faithfulness-of-newly-compiled (fraction of items that became compiling through repair and are faithful).
• Expectation: compile up, faithfulness of the new compilers low (consistent with the Beyond Compilation observation that Lean feedback gains are partly unfaithful [verify]).
• Tests H2.

E9. Schema-guided retrieval and proof guidance

• Data: 200 exercises with a reference statement and a dependency on at least one earlier definition or result in the same book; store built from the faithful, filtered items of the other books plus Mathlib docstrings.
• Arms: no retrieval; BM25 over statements; embedding retrieval; type-index (current search); find_solvable role coverage; oracle (gold dependencies).
• Provers: two open provers + one API model, pass@1 and pass@8, fixed timeout.
• Metrics: retrieval recall@k of gold dependencies; proof success; steps used.
• Controls: store filtered vs unfiltered (shows filtering matters downstream); store with shuffled roles (shows structure, not just text, matters).
• Tests H5.

E10. Contamination

• Procedure: string and normalized-statement match of each item against public Lean corpora and ProofNet; evaluate E4 on the clean subset; ask models to complete the item from the title only.
• Report: clean-subset deltas.

E11. Cost, time and reliability

• Report: tokens, USD, wall-clock and Lean time per page and per faithful item; failure counts per stage; silent-failure checks (the three faults the project found only on the server: empty-env key shadowing, container drift, overloaded unverified).

---

7. More detailed experiments (second layer, in priority order)

7.1 Role vocabulary and registry quality (S2)

• Growth curve of distinct roles vs items; duplicate-role rate before and after the reuse-before-create rule; human judgement on 200 role pairs the registry merged and 200 it kept apart (precision/recall of dedup).
• Effect of dedup on retrieval (E9 with and without dedup).

7.2 Nested simplices and the dependency graph (S3)

• Build the book's dependency graph from nesting; evaluate edge precision on 100 hand-labelled dependencies; test whether context-carrying formalization (feeding already-formalized definitions) fixes the "needs earlier definition" failures seen in E4.

7.3 Analogy mining (S4)

• Run AnalogySchemaMiner for N rounds; humans rate 200 proposed simplices as meaningful / forced; report acceptance rate and whether accepted simplices cover items previously degenerate (< 2 roles). Keep as optional/appendix: it must not hold up the main results.

7.4 Judge bias and cross-family control (S5)

• Full matrix: generator family x judge family; self-preference gap; alignment extractor family x generator family.

7.5 Robustness (S6)

• Page-image degradation (dpi, noise, rotation) vs detection and compile; prompt paraphrase robustness of S_T extraction (cf. robustness literature [verify]).

7.6 Statistical analysis plan

• All headline rates with Wilson 95% CIs; between-system differences by paired McNemar; gap CIs by bootstrap (10,000 resamples over items, clustered by book).
• Sample size: with 600 audited items, a proportion near 50% has about +-4 points half-width; a paired comparison with 20% discordance detects about a 6-point difference at 80% power (approximate; recompute with the observed discordance).
• Seeds: 3 for any sampled arm; report mean +- sd; no cherry-picked seed.
• Multiple comparisons: Holm correction across the pre-registered hypotheses H1-H5.

7.7 Cross-lingual and homogenization (S7)

• One Chinese-language textbook: detection, OCR, compile and faithful rates vs English.
• ACL 2027's optional theme (homogenization [verify theme wording on the final call]): do different models converge on the same wrong formalization? Measure agreement among wrong outputs across models.

7.8 Human effort (S8)

• Time to audit an item with page-grounded span and side-by-side simplices vs. with raw PDF and Lean code only (20 items x 2 annotators, crossover).

7.9 Budget (rough, recompute after pilot)

• Tokens: ~3k in + 1k out per formalization call; with ~1.5 calls per item average and 2,000 items per model per pass = about 9M tokens per model per pass; 5 models x 3 arms (E4/E7/E8) is about 135M tokens before judges. Judges and extraction add roughly 40%.
• Lean: about 10-30 s per item on the 4 cpu / 14 GiB runner; 2,000 items x 5 models x 3 arms is on the order of 100-250 CPU-hours, so use more than one runner or reduce the sample for arms E7/E8 to the 600 core.
• Human: 600 items x 2 annotators x ~3 min = 60 hours plus adjudication.

---

8. Work plan to 4 Jan 2027, risks, checklists

8.1 Timeline

Weeks	Dates	Work	Exit gate
1-2	21 Oct - 3 Nov	Fix unverified label, source_pages, incremental storage; port simplex (5.7); E0; choose books and confirm licences; annotation guideline	E0 >= 95%
3-4	4 - 17 Nov	Ingest all books (E1); build annotator tooling; recruit annotators; pilot 50 items	pilot kappa >= 0.6
5-6	18 Nov - 1 Dec	E2, E3, E4 runs; start labelling core	E4 table done
7-8	2 - 15 Dec	E5 labelling finished; E6, E7, E8; go/no-go 8 Dec	role alignment beats single judge on at least two error types, or fall back to an evaluation paper
9-10	16 - 29 Dec	E9, E10, E11; second-layer (7.1, 7.4) if time; figures	all main tables frozen 24 Dec
11	30 Dec - 3 Jan	Writing polish, checklist, artifact package, submit ARR by 3 Jan	submitted
Writing starts 1 Dec in parallel; related work and method sections can be drafted now.

8.2 Risks

Risk	Likelihood	Mitigation
Role alignment does not beat LLM judges	medium	Position as complementary and cheaper, with error localization; paper becomes evaluation + taxonomy
Annotators unavailable / slow	medium	Shrink core to 400; keep 150-item overlap; use project members for pilot
Archived simplex code needs more rework than planned	medium	Re-implement the minimal Role/Simplex/State in leanbench/ rather than porting everything; analogy miner stays optional
Compute for Lean at scale	medium	Second runner; reduce arms to core; cache by sha1(code)
Licensing blocks release	medium	Open books only; hashes-only for others
Overlap with Beyond Compilation, ShadowBench, Lean-GAP, ATLAS (all 2026)	high	Do not claim first textbook pipeline or first gap measurement. Claim role-level, authoring-free, human-calibrated localization + schema guidance + provenance/coverage. Compare against their metrics directly. Recheck arXiv weekly (search: autoformalization faithfulness, textbook Lean) until submission
ShadowBench finds the gap is small on short ProofNet-style targets (2.1 pts)	medium	Stratify E4 by statement length/complexity and report where role alignment helps; do not generalise from long items to all items
Dates shift	low-medium	ICML/NeurIPS dates are projected; recheck CFPs monthly

8.3 ACL / ARR checklist

Limitations section (LLM dependence of S_T, one formal system, few books, annotator expertise); Responsible NLP checklist (compute, licences, annotator pay and instructions); data statement for the release; reproducibility package (pinned image, prompts, seeds, scripts); no author-identifying text in artifacts; anonymized repository for review.

8.4 Deliverables

docs/research-plan.md (this file); registry + projection + alignment code with tests; annotation tool; dataset release package (licence-clean); paper draft.

---

9. Sources checked on 2026-10-21

• ACL 2027 site: ARR 4 Jan 2027; Kyoto 20-22 Aug 2027.
• NAACL 2027 call (ARR 12 Oct 2026, closed); ICLR 2027 call (25 Sep 2026, closed); CPP 2027 page (10 Sep 2026, closed); ITP 2027 site (Glasgow, early Aug 2027, deadlines pending).
• Aggregators (unofficial, projected): ICML 2027, IJCAI 2027, COLM 2027, NeurIPS 2027.
• Literature: ProofNet; Poiroux et al.; FormalAlign; Beyond Compilation; ShadowBench.
• Local: lean-bench repo, runs/p85-110, archived/schema-simplex.