Skip to content

Commit 9e43a87

Browse files
cknollcknoll
committed
feat(authoring): Lean-theorem import substrate + 3 validation runs
Squash-merge of branch lean-content-import: a Claude-Code-native authoring substrate that imports formal statements into pyirk content modules, with a Lean/mathlib4 source adapter as the first frontend. Core (src/pyirk/authoring/): retrieval-first prompting with a worked example, structured append + round-trip validation via irkloader, claude -p subprocess with JSON cost tracking, mandatory FORK escalation for ambiguous modeling, and pipeline-owned guards for the failure classes surfaced by three bulk runs: key-collision remapping, non-ASCII Lean operators, scope-reopen, and retryable timeouts. CLI (pyirk --import-lean): single/--all import, unattended --fork-policy, per-theorem --stats-jsonl, --keep-going, --resume, --limit; plus a mocked dry-run tool and a regression guard for the irkloader reuse_loaded short-circuit. The three bulk-run evaluations are kept as bulk_runs*/SUMMARY.md (66/89 -> 80/89 ok across runs; the raw generated modules/stats/logs are intentionally left on the lean-content-import branch). Full suite green: 223 passed, 12 skipped, 2 xfailed. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> # Last 3 commits: # c10d298 feat(cli): seed bootstrapped config with commented nemo-delegation block # e247a6d feat(cli): show config file path in --help output # d2d921c feat(nemobridge): persistent opt-in for nemo delegation via pyirk config
1 parent c10d298 commit 9e43a87

17 files changed

Lines changed: 4465 additions & 7 deletions

‎bulk_runs/SUMMARY.md‎

Lines changed: 158 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
# Bulk-Run Summary: Three Lean-Import Corpora
2+
3+
Generated from stats files in `bulk_runs/{eigenspace,trace,ode_transform}/stats.jsonl`.
4+
De-duplication: first record per `(namespace, theorem)`.
5+
6+
---
7+
8+
## A. Per-Corpus Metrics
9+
10+
| Corpus | Total | ok | failed | error | Fork rate | Val-retry rate | Mean dur (s) | Max dur (s) |
11+
|--------|-------|----|--------|-------|-----------|----------------|--------------|-------------|
12+
| eigenspace | 35 | 20 | 14 | 1 | 80.0 % (28/35) | 60.0 % (21/35) | 315.9 | 792.6 |
13+
| trace | 35 | 27 | 8 | 0 | 68.6 % (24/35) | 34.3 % (12/35) | 229.5 | 793.6 |
14+
| ode_transform | 19 | 19 | 0 | 0 | 31.6 % (6/19) | 10.5 % (2/19) | 180.9 | 394.1 |
15+
16+
- **Fork rate**: fraction of unique theorems with at least one `fork` event.
17+
- **Val-retry rate**: fraction with at least one `validation_fail` event.
18+
19+
---
20+
21+
## B. Fork Questions
22+
23+
All fork events from first-occurrence records.
24+
25+
| # | Corpus | Theorem | Question (abbreviated) | Chosen |
26+
|---|--------|---------|------------------------|--------|
27+
| 1 | eigenspace | mem_genEigenspace | Existential `∃ l ≤ k, x ∈ ker((f−μ•1)^l)` — no native binder in `new_equation`. Which encoding? | a |
28+
| 2 | eigenspace | genEigenspace_directed | `Directed (· ≤ ·)` predicate on submodule family — no match in index. How to represent? | a |
29+
| 3 | eigenspace | mem_genEigenspace_nat | Both iff sides are set-membership `x ∈ S`; `new_equation` needs expression equality. How? | a |
30+
| 4 | eigenspace | mem_genEigenspace_top | Same — both sides are set-membership propositions. How to encode the biconditional? | a |
31+
| 5 | eigenspace | genEigenspace_eq_iSup_genEigenspace_nat | RHS `⨆ l : {l : ℕ // l ≤ k}` — how to encode bounded-index supremum? | a |
32+
| 6 | eigenspace | genEigenspace_top | How does `I10` relate to the unbounded `⨆ k : ℕ`? Arity-2 reuse or new item? | a |
33+
| 7 | eigenspace | genEigenspace_one | Unconditional equality — no logical premise exists. How to structure setting/premise/assertion? | a |
34+
| 8 | eigenspace | mem_genEigenspace_zero | `0 : M` (module zero) — reuse `ma.I5000["scalar zero"]` or new module-zero item? | a |
35+
| 9 | eigenspace | genEigenspace_zero | `⊥` (trivial submodule) — new named constant vs. structural `ker(id)` vs. scalar zero proxy? | a |
36+
| 10 | eigenspace | UnifEigenvalues.mk_val | `⟨μ.val, μ.property⟩ = μ` requires subtype constructor; proof term not representable. How? | a |
37+
| 11 | eigenspace | HasUnifEigenvector.hasUnifEigenvalue | `HasUnifEigenvector(f,μ,k,x)` is 4-ary; pyirk tops out at arity 3. How to encode? | a |
38+
| 12 | eigenspace | HasUnifEigenvector.apply_eq_smul | Type of `x : M` in setting — `ma.I7151["vector"]` vs. new "module element" item? | a |
39+
| 13 | eigenspace | HasUnifEigenvector.pow_apply | `n : ℕ` (plain nat) vs. `I3["extended natural number"]` (ℕ∞). New subclass or reuse? | a |
40+
| 14 | eigenspace | HasUnifEigenvalue.exists_hasUnifEigenvector | `∃ v, HasUnifEigenvector μ k v` — how to encode existential in assertion scope? | a |
41+
| 15 | eigenspace | HasUnifEigenvalue.isNilpotent_of_isNilpotent | `IsNilpotent` appears on both endomorphism and scalar — one abstract predicate or two typed items? | a |
42+
| 16 | eigenspace | HasUnifEigenvalue.mem_spectrum | `μ ∈ spectrum R f` — spectrum not in index. Set-valued operator + membership, or binary predicate? | a |
43+
| 17 | eigenspace | genEigenspace_div | `a / b` as eigenvalue — no scalar division in module. New binary operator? | a |
44+
| 18 | eigenspace | genEigenrange_nat | Two new operators analogous to existing kernel/eigenspace — standalone or shared parent type? | a |
45+
| 19 | eigenspace | HasUnifEigenvalue.exp_ne_zero | `k ≠ 0` — disequality, not equation. New `is_nonzero` predicate or `not_equal` operator? | a |
46+
| 20 | eigenspace | genEigenspace_top_eq_maxUnifEigenspaceIndex | `[IsNoetherian R M]` typeclass — subtype in setting or boolean predicate in premise? | a |
47+
| 21 | eigenspace | genEigenspace_top_eq_maxUnifEigenspaceIndex | (retry) Same Noetherian constraint — two new items or one boolean predicate? | a |
48+
| 22 | eigenspace | genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex | Submodule-ordering assertion `≤` — new `I_sle` operator or relation? | a |
49+
| 23 | eigenspace | genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le | Premise is `maxUnifEigenspaceIndex ≤ k`. New `leq` + `maxUnifEigenspaceIndex` operators? | a |
50+
| 24 | eigenspace | HasUnifEigenvalue.lt | `0 < m` — new "positive extended natural" subtype or explicit `<` predicate in premise? | a |
51+
| 25 | eigenspace | hasUnifEigenvalue_iff_hasUnifEigenvalue_one | `hk : 0 < k ⊢ … ↔ …` — positivity side condition + iff. Use subtype for k or two-equation premise? | a |
52+
| 26 | eigenspace | maxUnifEigenspaceIndex_le_finrank | Inequality conclusion `≤ finrank K V`. New `leq_nat` boolean operator? | a |
53+
| 27 | eigenspace | genEigenspace_le_genEigenspace_finrank | Submodule containment `≤`. New relation `R_is_submodule_of` or boolean operator? | a |
54+
| 28 | eigenspace | genEigenspace_eq_genEigenspace_finrank_of_le | `finrank K V` as callable expression — new unary "finite rank" operator? | a |
55+
| 29 | eigenspace | genEigenspace_eq_genEigenspace_finrank_of_le | (retry) `finrank K V` — unary operator on endomorphism vs. explicit dimension variable? | a |
56+
| 30 | eigenspace | mapsTo_genEigenspace_of_comm | `Commute f g` (premise) + `MapsTo g S S` (assertion) — composition equation or boolean predicates? | a |
57+
| 31 | eigenspace | mapsTo_genEigenspace_of_comm | (retry) `MapsTo g S S` — general ternary predicate or binary `is_invariant_under`? | a |
58+
| 32 | trace | traceAux_def | `Matrix.trace` — bare unary operator or share parent type with `ma.I5359["determinant"]`? | a |
59+
| 33 | trace | traceAux_eq | Functional equality `traceAux R b = traceAux R c`. Expand pointwise (∀ f) or treat as function-object? | a |
60+
| 34 | trace | trace_eq_matrix_trace_of_finset | `LinearMap.trace` (distinct from traceAux) — new item `I3009` or reuse traceAux? | a |
61+
| 35 | trace | trace_eq_matrix_trace | `I3005["linear map to matrix"]` — arity 2 or arity 3 (two basis args)? | a |
62+
| 36 | trace | trace_mul_comm | `f * g` (composition) — new `I3012` item or use pyirk's overloaded `*`? | a |
63+
| 37 | trace | trace_lie_mul_eq | Lie bracket `⁅f,g⁆` — domain-specific or abstract Lie algebra item? | a |
64+
| 38 | trace | trace_conj | `f : (M →ₗ M)ˣ` invertible endomorphism — new subtype item + inverse operator? | a |
65+
| 39 | trace | trace_eq_contract_of_basis | `dualTensorHom` and `contractLeft` — minimal untyped, full type hierarchy, or domain-only? | a |
66+
| 40 | trace | trace_eq_contract_of_basis' | `dualTensorHomEquivOfBasis` — new standalone item or specialisation of existing `I3022`? | a |
67+
| 41 | trace | trace_eq_contract | Function equality `trace ∘ₗ dualTensorHom = contractLeft` — new compose operator or pointwise? | a |
68+
| 42 | trace | trace_eq_contract' | Unapplied map equality with `dualTensorHomEquiv` (not `dualTensorHom`) — how to encode? | a |
69+
| 43 | trace | trace_one | Ring `R` and module `M` typing — new "commutative ring"/"R-module" items or narrow to field? | a |
70+
| 44 | trace | trace_id | Unconditional `trace(id) = finrank` — `p.I15` with premise constraints or bare proposition? | a |
71+
| 45 | trace | trace_transpose | Function-level equality `trace_dual ∘ transpose = trace_M` — new transpose item, pointwise encoding? | a |
72+
| 46 | trace | trace_prodMap | `prodMapLinear`, `prodMap`, `coprod id id` — 4 new items, 2 items, or 1 + opaque? | a |
73+
| 47 | trace | trace_tensorProduct | `trace(f⊗g) = trace(f)·trace(g)` via `compr₂`/`compl₁₂`/`mapBilinear`/`lsmul` — literal structure or semantic shortcut? | a |
74+
| 48 | trace | trace_comp_comm | `f : M →ₗ N`, `g : N →ₗ M` (non-endo) — new "linear map between modules" type or reuse endomorphism? | a |
75+
| 49 | trace | trace_conj' | `e : M ≃ₗ N` (cross-module isomorphism) — new "linear isomorphism between modules" supertype? | a |
76+
| 50 | trace | IsProj.trace | `IsProj p f` projection condition — new "submodule" item + binary predicate, or bake into `f` type? | a |
77+
| 51 | trace | IsIdempotentElem.trace_eq_zero_iff | Char-zero comm ring + idempotency — new ring/module items or approximate with field? | a |
78+
| 52 | trace | isNilpotent_trace_of_isNilpotent | `IsNilpotent` on endomorphism (premise) and scalar (assertion) — two subtype items or one predicate? | a |
79+
| 53 | trace | trace_comp_eq_mul_of_commute_of_isNilpotent | `IsNilpotent(g − μ·id)` in premise — predicate-as-equation or nilpotent-subtype in setting? | a |
80+
| 54 | trace | trace_baseChange | `f.baseChange A` — new standalone binary operator, or derive from `I3041["tensor product of linear maps"]`? | a |
81+
| 55 | trace | Module.Free.bijective_algebraMap_of_finrank_eq_one | `Function.Bijective (algebraMap R S)` — boolean predicate item or bijective-hom subtype? | a |
82+
| 56 | ode_transform | IsIntegralCurveOn.comp_add | `IsIntegralCurveOn(γ,v,s)` — new class with instance-of idiom, or ternary predicate returning truth? | a |
83+
| 57 | ode_transform | isIntegralCurveOn_comp_sub | Sub-variant operators: reuse I1006/I1007 with negated arg, or new `I1008`/`I1009`? | a |
84+
| 58 | ode_transform | isIntegralCurveAt_comp_add | `t₀ - dt` in setting — use `st.t0 - st.dt` directly or new `vadd neg on real point` item? | a |
85+
| 59 | ode_transform | IsIntegralCurve.comp_add | `IsIntegralCurve γ v` (no domain) — new binary predicate `I1013` or reuse `I1005` with `Set.univ`? | a |
86+
| 60 | ode_transform | IsIntegralCurveOn.comp_mul | `a • v ∘ (· * a)` scaling + precomposition — two new operator items or one combined? | a |
87+
| 61 | ode_transform | isIntegralCurve_const | Constant curve + `∀t, v t x = 0` — three new items (curve, eval, zero-vector) or collapsed predicate? | a |
88+
89+
---
90+
91+
## C. Failure Classification
92+
93+
| Corpus | Theorem | Outcome | Apparent error class |
94+
|--------|---------|---------|----------------------|
95+
| eigenspace | genEigenspace_directed | failed | `ValueError`: label mismatch (`'proposition'` used as scope label instead of `'scope'`) |
96+
| eigenspace | mem_genEigenspace_nat | failed | `TypeError`: `I5["iterated-kernel existential formula"]` not callable (no `_custom_call`) |
97+
| eigenspace | mem_genEigenspace_top | error | `TypeError`: same — `I5` not callable; combined with timeout on attempt 2 |
98+
| eigenspace | mem_genEigenspace_zero | failed | `TypeError`: evaluated-mapping item `Ia98516` not callable |
99+
| eigenspace | genEigenspace_zero | failed | `AssertionError`: item index `I17` already occupied (index collision) |
100+
| eigenspace | genEigenspace_div | failed | `SyntaxError`: Unicode bullet `•` (U+2022) in generated Python |
101+
| eigenspace | genEigenspace_top_eq_maxUnifEigenspaceIndex | failed | `AssertionError`: item `I73` already occupied (index collision cascade) |
102+
| eigenspace | genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le | failed | `AssertionError`: `I73` already occupied |
103+
| eigenspace | HasUnifEigenvalue.le | failed | `TypeError`: `I31["less-or-equal-than-relation"]` not callable |
104+
| eigenspace | HasUnifEigenvalue.lt | failed | `AssertionError`: `I73` already occupied |
105+
| eigenspace | hasUnifEigenvalue_iff_hasUnifEigenvalue_one | failed | `AssertionError`: `I80` already occupied |
106+
| eigenspace | maxUnifEigenspaceIndex_le_finrank | failed | `AssertionError`: `I73` already occupied |
107+
| eigenspace | genEigenspace_le_genEigenspace_finrank | failed | `AssertionError`: `I73` already occupied |
108+
| eigenspace | genEigenspace_eq_genEigenspace_finrank_of_le | failed | `AssertionError`: `I73` already occupied |
109+
| eigenspace | mapsTo_genEigenspace_of_comm | failed | `AssertionError`: `I73` already occupied |
110+
| trace | trace_eq_contract_of_basis' | failed | `TypeError`: evaluated mapping for `dualTensorHomEquivOfBasis(b)` not callable |
111+
| trace | trace_id | failed | `TypeError`: `I3031["identity linear endomorphism"]` not a class (cannot be instantiated) |
112+
| trace | trace_conj' | failed | `AssertionError`: `I3051` already occupied (index collision cascade) |
113+
| trace | IsProj.trace | failed | `AssertionError`: `I3051` already occupied |
114+
| trace | IsIdempotentElem.trace_eq_zero_iff | failed | `AssertionError`: `I3051` already occupied |
115+
| trace | trace_comp_eq_mul_of_commute_of_isNilpotent | failed | `AssertionError`: `I3051` already occupied |
116+
| trace | trace_baseChange | failed | `AssertionError`: `I3051` already occupied |
117+
| trace | Module.Free.bijective_algebraMap_of_finrank_eq_one | failed | `AssertionError`: `I3060` already occupied (same cascade) |
118+
119+
**ode_transform**: no failures.
120+
121+
---
122+
123+
## D. Qualitative Observations
124+
125+
- **Strong intra-module reuse.** Later theorems consistently reference items created by earlier ones.
126+
In `lean_eigenspace.py` the ternary operator `I4["generalized eigenspace operator"]`, unary
127+
`I7["linear map kernel"]`, constant `I8["identity endomorphism"]`, and accumulating index-set /
128+
supremum items (I10, I12, I14, I19, …) are reused across many subsequent theorem items. In
129+
`lean_ode_transform.py` the predicates `I1005["IsIntegralCurveOn"]`, `I1010["IsIntegralCurveAt"]`,
130+
and operators `I1006`/`I1008`/`I1014`/`I1015` carry through every comp-variant theorem.
131+
132+
- **ode_transform: separate operators per variant, not merged structure.**
133+
Despite `comp_add`, `comp_sub`, `comp_mul`, and `comp_neg` all being shifts of the same integral-
134+
curve predicate, the LLM did **not** create a single parameterised "composition transform" operator.
135+
It introduced a distinct pair of operators per arithmetic operation
136+
(e.g. `I1006`/`I1007` for add, `I1008`/`I1009` for sub, `I1014`/`I1015`/`I1016` for mul). The
137+
shared predicate `I1005["IsIntegralCurveOn"]` is reused everywhere, but the transformation
138+
operators themselves are not merged.
139+
140+
- **Dominant failure mode: index collision cascade.**
141+
In both eigenspace and trace, a single early theorem attempt that chose (but then collided on) a
142+
specific item number (e.g. `I73` in eigenspace, `I3051` in trace) causes all subsequent theorems
143+
that independently try to create a new item at the same index to fail immediately with
144+
`AssertionError: … already occupied`. This is a cumulative-state artifact: once a partial
145+
(failed) run occupies slot N, every retry and all later theorems that also want slot N are blocked.
146+
147+
- **Surprising outcome-rate gap across corpora.** ode_transform achieved 100 % success (19/19 ok)
148+
with low fork and validation-fail rates (32 % / 11 %). The eigenspace corpus had only 57 % success
149+
with 80 % fork rate and 60 % validation-fail rate. The structural difference is that ODE-transform
150+
theorems share a single repeated pattern (`IsIntegralCurveOn/At/curve`, precompose, shift), whereas
151+
eigenspace theorems involve increasingly exotic type-class constraints (Noetherian, nilpotent,
152+
disequalities, lattice bottoms) for which pyirk has no direct encoding primitive.
153+
154+
- **Duration outliers at timeout boundary.** Both eigenspace and trace contain records with
155+
`duration_s` close to 792–793 s, flagged as `TimeoutExpired` errors. These represent theorems
156+
where the LLM ran out of time mid-attempt (apparently after a fork decision triggered a more
157+
complex encoding path), while all ode_transform theorems finished well under 400 s. The timeout
158+
boundary appears to be approximately 800 s.

0 commit comments

Comments
 (0)