Analysis plan (pre-registered before any run on `test`)

Written 2026-11-03, during Phase 8 Part A, before any configuration was run on the test split. It fixes the metrics, tests and handling rules so that the analysis does not depend on the results. Any later change must be recorded at the end of this file with its date and reason, and reported in the paper as a deviation.

Notation and equations refer to the report (docs/report/Proyecto_Inteligencia.pdf, Section IV-A).

1. Data and design

Problems: data/eval.jsonl, split test: 30 problems, stratified on the 3 × 3 grid (difficulty easy/medium/hard × area algebra/number theory/combinatorics, with the documented reallocation of Phase 7). The split was fixed with seed 2026 before any prompt tuning.
Configurations: C1–C5 (Section IV-A8), all on the same LangGraph graph, profile experiment (deepseek-flash, config/models.yaml), seed 2026, with the configuration frozen by the team's commit at the end of Part A (its hash is recorded in each run_config.json).
Run order on test: C5, C3, C4, C2, C1 (team decision 2026-10-31).
One run per (configuration, problem). No configuration is re-run on test to obtain a better result. The only exception is the provider_error rule of Section 5.
Paired design: every configuration sees the same 30 problems, so comparisons between configurations are paired by problem.
The LLM response cache stays on. Identical requests across configurations (e.g. the first attempt of C4 and C5) are answered from the cache; this keeps the paired comparison tighter and is stated in the paper. Costs are compared with the nominal cost (cost_usd_nominal: cache hits priced as fresh calls) so that run order does not favour later configurations.

2. Primary outcome

Verified success of configuration m on problem x: Acc(φ_x, c*_x) of Eq. 2 for the final assembled proof (status solved in results.jsonl). Only the Lean kernel decides (RNF-1).
Success rate: SR_m = (number solved) / 30, with a Wilson 95 % interval.
Since each problem is run once, pass@k of Eq. 15 is estimated only for k = 1 (= SR_m). This is stated as a limitation; no repeated sampling is run.

3. Planned comparisons (confirmatory)

Three comparisons, decided now, each a two-sided exact McNemar test on the paired outcomes (binomial test on the discordant pairs b, c with p = 1/2), Bonferroni-corrected for 3 tests (reject at p < 0.05 / 3 ≈ 0.0167; adjusted p-values = min(1, 3p) are also reported):

ID	Comparison	Question
H1	C5 vs C1	Does the multi-agent pipeline beat direct proof prompting (at equal mean measured computation, `b_max` of C1 fixed in Part A)?
H2	C5 vs C3	RAG contribution, Δ_RAG = SR_C5 − SR_C3 (Section IV-A9e).
H3	C5 vs C4	Contribution of the Critic loop (retries and replanning).

For each one we report: b and c (discordant counts), ΔSR, a 95 % paired bootstrap interval for ΔSR (10 000 resamples of problems, seed 2026, percentile method), the exact p-value and the Bonferroni-adjusted p-value. With n = 30 the power is low; a non-significant result is reported as "no evidence of a difference", never as "no difference".

Exploratory only (no correction, labelled exploratory, no claims): C3 vs C4, C1 vs C3, C1 vs C4, and any per-difficulty or per-area comparison.

C2 is not compared with McNemar on verified success: its success is self-assessed, not verified.

4. Secondary outcomes

Per cell of the 3 × 3 grid: for each configuration, solved / n of each (difficulty, area) cell, with the cell's n shown. Descriptive only: no tests and no intervals per cell (n ≤ 5). Margins by difficulty and by area are reported with Wilson intervals. Empty cells (no easy combinatorics) are shown as "—".
Baseline B (Eq. 16): claimed rate |B⁺| / 30 (Wilson), and FPR_B = |{x ∈ B⁺ : ¬Acc}| / |B⁺| (Wilson), where every self-assessed proof is passed to the Autoformalizer–Verifier loop with the same budget (run_baseline_b.py --check, to be built before the C2 run on test). FPR_B is an upper bound on the true false-positive rate; a manual review of the B⁺ problems that fail formalization (all of them if ≤ 10, otherwise 10 drawn with seed 2026) separates wrong informal proofs from formalization failures.
Efficiency (Section IV-A9c, RNF-3): per configuration, C̄_solved = Σ_x C(x) / #solved (failed problems' calls included in the numerator), and the same ratio for tokens, nominal USD cost and wall-clock time; also the means per problem. 95 % bootstrap intervals (resampling problems). RNF-3 (C̄_solved ≤ 20) is checked for C5 and reported as met or not; it is not tuned.
Refinement robustness (Eqs. 14, IV-A9d): SR(k) for k = 1, 2, 3, where a C5 problem counts as solved at k if its accepted proof used at most k attempts on every subgoal (read from trace.jsonl); k = 1 is also reported from C4. Δ̂(k) = SR(k) − SR(k−1) is plotted against the independence curve of Eq. 14 with p_i estimated from first-attempt subgoal success in C5. The paper states that k = 1 from C4 has no retries or advice while k = 2, 3 come from C5.
Error taxonomy (Section IV-A9f): relative frequency of each κ class of Eq. 11 over all failed attempts, per configuration and per area; separately, the final failure reason per problem (stage and final status). C1 attempts are classified with the same κ.

5. Status handling

Status in `results.jsonl`	Meaning	Primary analysis
`solved`	Acc holds on the assembled proof	success
`failed` (any `stage`)	the method did not find an accepted proof	failure
`budget_exhausted`	`b_max` LLM calls reached	failure (the budget is part of the method)
`timeout` / memory limit	Lean verification limits	failure
`error` / `node_error` / `invalid_statement`	a bug in the system or the statement	failure; counted and listed
`provider_error`	the API refused or failed after all transport retries	see below
`budget_stop`	the project or run spend cap stopped the run	see below
run status `lean_unavailable`; row with `lean_down: true`	Lean could not load Mathlib (start-up probes)	as `provider_error`: infrastructure; re-run once, see below

provider_error is an infrastructure failure, not a decision of the model. After a run, the problems with provider_error are re-run once, in a new run folder with the same configuration and cache (the original run is kept untouched). The re-run's result replaces the provider error in the analysis. If it is again provider_error, it counts as a failure in the primary analysis, and a sensitivity analysis excludes those problems from that configuration (and, for McNemar, the pairs where either side is excluded). Counts are reported per configuration.
budget_stop: the problem and the rest of the run were not attempted. The team decides whether to raise the spend cap; if raised, only the problems not attempted are run with the same frozen configuration and merged. If not, that configuration is reported as incomplete: SR on the attempted problems (with n stated), a conservative SR counting not-attempted problems as failures, and McNemar only on the problems attempted by both configurations.
Lean unavailable: a run that stops with lean_unavailable made no LLM call for the problems not run; those problems, and a row marked lean_down: true (Lean was lost during it, so its failure may be Lean's), are re-run once with the same configuration, exactly like provider_error. A success in a lean_down row stands (the kernel accepted it).
Runs marked degraded (Lean file back-end used) are valid and are flagged in the tables.

6. Fidelity notes (manual check before reporting success)

data/curation/fidelity_review.yaml lists, under notes, problems whose formal statement differs from the informal text in a way judged harmless at curation time. Every problem solved on test by any configuration that has a note is reviewed by hand before it is counted as a success in the paper (PLAN.md, Phase 9). The review records whether the accepted proof establishes what the informal problem asks. The verified SR (Section 2) is never changed by this review: the kernel's verdict is what it is. If a review concludes that the formal statement does not capture the informal problem, the paper reports it next to the table (problem, configuration, reason) and gives the SR both with and without that problem.

7. What is reported, in order

Table: SR with Wilson 95 % CI for C1, C3, C4, C5; claimed rate and FPR_B for C2.
Table: H1–H3 with b, c, ΔSR, bootstrap CI, exact p and Bonferroni-adjusted p.
Table: per-cell solved/n for each configuration, with difficulty and area margins.
Table: efficiency (calls, tokens, nominal cost, time per problem and per solved problem).
Figure: SR(k), k = 1…3, vs the independence curve of Eq. 14.
Figure or table: κ taxonomy per configuration and area.
Counts of provider_error, budget_stop, error, degraded runs and the fidelity reviews.

Analysis code (src/formal_mas/analysis/stats.py, scripts/compare.py) is written in Phase 9 to implement exactly this plan; it is tested on dev runs before it reads any test result.

Exploratory analysis (post hoc, decided 2026-11-08)

Decided after all confirmatory test runs and their analysis were finished. It is exploratory and changes no result, test or conclusion of §2–§7.

Motivation. The hard problems look limited by the model rather than by the method: C1 and C5 solve the same 4 of the 10 hard test problems (imo_1964_p1_2, imo_1965_p2, putnam_1964_b2, putnam_1965_b2), so the agents add nothing on that stratum with DeepSeek-Flash.
Run. C5 exactly as frozen for the main runs (same graph, prompts, pipeline.yaml method settings, seed, B_max/b_max), with model profile experiment_pro: identical to experiment except that every role uses deepseek-v4-pro instead of deepseek-flash (config/models.yaml). Input: the 10 hard test problems, all of them (not only those C5-Flash failed), as a file with exactly those lines of data/eval.jsonl in dataset order; its sha256 and id list go in run_config.json. One run, --run-usd 5.00; if it ends in budget_stop it is not resumed and the problems without a complete row are reported as not attempted.
Reported. A descriptive paired table, problem by problem, C5-Flash (the kept rows of the main C5 test result, §Deviations) vs C5-Pro on the same 10 problems: solved, LLM calls, cost (real and nominal), wall time in minutes; plus totals. The 2×2 table of solved/not solved may be shown as counts.
Not done. No hypothesis test, CI or p-value; nothing is added to the Bonferroni family; no claim about Pro beyond these 10 problems. Pro's results never replace C5's in any main table.
Fidelity. Any new success gets the same manual fidelity check as §6 before it is reported.

Deviations

No deviation from the analysis itself. Infrastructure incidents during the test runs:

2026-11-03, C5 on test interrupted by low memory. Run 20261103T174646Z_C5_experiment (commit ad70ec2, clean tree) was killed at about 19:16 UTC by the host (Claude Code stops background jobs when the machine runs critically low on memory; the Lean REPL, ~3.5 GB, was sharing RAM with an idle Lean language server, ~2.7 GB). It is an infrastructure failure, not a decision of the method. 23 of 30 problems had finished and are kept unchanged; the 24th (imo_1987_p6) was cut mid-problem and left no row in results.jsonl. No row was lean_down, and there was no provider_error or budget_stop. The 7 problems without a row were completed in two resume runs. Both used the same frozen configuration (the analysis is the same at either commit), the same seed and cache, and the language server was stopped first. The input of each is a file holding exactly the needed lines of data/eval.jsonl, unchanged and in the original order. Its sha256 and the id list are in that run's run_config.json, and a copy is kept as test_remaining.jsonl in that run's folder.
1. 20261103T212359Z_C5_experiment_resume (commit ad70ec2, clean tree; input sha256 53284f8f…086fc4) ran all 7 from scratch: imo_1987_p6, imo_1979_p1, imo_1984_p6, imo_1964_p1_2, putnam_1964_b2, putnam_1995_b1, putnam_1965_b2. It reached its spend cap (--run-usd 0.50) during the third problem. imo_1987_p6 and imo_1979_p1 finished (both failed). imo_1984_p6 got a budget_stop row after 19 calls, and the last 4 were not attempted.
2. 20261103T225140Z_C5_experiment_resume2 (commit 93bc701, which changes only this file; clean tree; input sha256 f3da0f6d…6d77f91) ran imo_1984_p6 from scratch, plus the 4 problems not attempted, with --run-usd 1.00 (the cap raised by team decision, §5). The requests that imo_1984_p6 repeats from step 1 are answered from the cache. Merge: the C5 result on test has one row per problem (30 in all), taken from the run where the problem finished:
- 23 rows from the first run;
- imo_1987_p6 and imo_1979_p1 from resume 1;
- imo_1984_p6 and the other 4 from resume 2. The budget_stop row of imo_1984_p6 in resume 1 is discarded; only its complete row counts. The spend of the discarded attempts (imo_1987_p6 in the first run and imo_1984_p6 in resume 1) counts towards the project's real cost. It is not in any kept row, so each problem's efficiency figures come from its kept row only. Cache hits lower the real cost of the resume runs but not their nominal cost, and nominal cost is the figure compared (§1).
2026-11-03, run order C4 before C3. C4 was run right after C5, and C3 moved to the next off-peak morning, so the order is C5, C4, C3, C2, C1 instead of C5, C3, C4, C2, C1 (§1). The reason is schedule and cost only. C3 takes about 3 h and would have run into the provider's peak window (01:00 UTC), while C4 is short and is answered mostly from the cache of C5. This has no effect on the analysis. Each configuration is still run once on the same 30 problems with the same frozen configuration, and the comparisons are paired by problem. C4 shares its cached requests with C5, not with C3, so its cache hits are the same in either order. Costs are compared at nominal prices (§1), so run order does not favour either configuration.
2026-11-04, per-run spend cap raised from 1.0 to 2.0 USD before C3 on test. Team decision. Only config/pipeline.yaml → spend.run_usd changed (1.0 → 2.0); run_eval.py --run-usd can only lower that cap, so C3 (about 3 h, no cache shared with C5 because its prompts carry no lemmas; C5 on test cost 1.36 USD real in total) would otherwise very likely end in budget_stop before the 30th problem. This is a spend-control change, not a method change: the cap is checked before each paid request and only decides whether the request is sent, so it does not change any prompt, model, budget B_max/b_max, policy or result of a request that is sent. The project cap spend.total_usd stays at 9.0 USD. C5 and C4 ran under the 1.0 USD cap (or a lower --run-usd); C3 runs with --run-usd 2.00. The offline test that pins the configured caps (tests/test_spend.py::test_real_pipeline_yaml_has_the_caps) was updated to the new value.
2026-11-05, per-run spend cap raised from 2.0 to 3.5 USD before C1 on test. Team decision. Only config/pipeline.yaml → spend.run_usd changed (2.0 → 3.5). C1 costs more per call than C5 (the cost run 20261103T161957Z_C1_experiment_c1_cost spent 0.21 USD real on 3 dev problems, about 0.07 USD per problem), so 30 problems would likely end in budget_stop under 2.0 USD. As before, this is a spend-control change, not a method change: the cap is checked before each paid request and only decides whether the request is sent, so it does not change any prompt, model, budget B_max/b_max, policy or result of a request that is sent. The project cap spend.total_usd stays at 9.0 USD. C1 runs with --run-usd 3.50. The offline test that pins the configured caps was updated to the new value.
2026-11-05, C1 on test stopped by the team. Run 20261105T131443Z_C1_experiment (commit 5ed7507, clean tree, --run-usd 3.50) was stopped on purpose at about 17:43 UTC, together with its whole process tree (REPL, lake), to free the machine for other work. It is an operational incident, not a decision of the method: no code, prompt, model or configuration changed. 23 of 30 problems had finished and are kept unchanged; the 24th (imo_1987_p6) was cut mid-problem (after 10 calls, 0.10 USD real) and left no row in results.jsonl. There was no provider_error or budget_stop. The 7 problems without a row will be completed in a resume run, following the same procedure as for C5 (same frozen configuration, seed and cache; input file with exactly the needed lines of data/eval.jsonl; imo_1987_p6 run from scratch, its earlier spend counted in the project's real cost but in no kept row). The resume run is 20261107T200233Z_C1_experiment_resume (commit 2c8eae5, clean tree; input sha256 009bece56dc0fdde3c814c9e81aeda6ee7bd8dd677d0fa29bab5dd723c907b8b, the 7 problems in dataset order; --run-usd 1.65 = 3.50 minus the 1.8407 USD C1 had spent, rounded down, so that C1 as a whole stays under 3.50).
2026-11-07, dirty: true in four run_config.json files (recording artefact, found in the analysis). run_eval.py rewrites run_config.json when a run ends, and the git state (and created_utc) were read again at that moment instead of at launch. In 20261103T212359Z_C5_experiment_resume, 20261103T225140Z_C5_experiment_resume2, 20261103T235556Z_C4_experiment and 20261107T200233Z_C1_experiment_resume the only changed file is docs/analysis_plan.md, edited while the run was going to log these very incidents; every tree was clean at launch (checked before each run, as the Phase 8 rules require). No code, prompt, configuration or data file changed, so the method is not affected. In those files created_utc is also the end time; the start is the timestamp in the run name and the run_start event of trace.jsonl. The two interrupted runs (20261103T174646Z_C5_experiment, 20261105T131443Z_C1_experiment) never reached the final rewrite and show their launch state. Fixed after all test runs (run_config.run_start_info): git and created_utc now describe the launch, and the state when the file is written goes to git_end and written_utc. Runs already made are not rewritten.
2026-11-08, spend caps raised for the exploratory C5-Pro run (spend control). Team decision, after all confirmatory test runs. Only config/pipeline.yaml → spend changed: total_usd 9.0 → 12.5 and run_usd 3.5 → 5.0. The ledger stood at 7.36 USD; re-pricing C5-Flash's tokens on the 10 hard test problems at Pro prices gives about 3.75 USD off-peak (7.49 USD at peak), so the old caps would stop the run. As before, the caps are checked before each paid request and only decide whether it is sent; no prompt, model of the main profiles, budget B_max/b_max, policy or result changes, and no confirmatory run is repeated. The run uses --run-usd 5.00. The offline test that pins the configured caps (tests/test_spend.py::test_real_pipeline_yaml_has_the_caps) was updated to the new values.
2026-11-08, exploratory C5-Pro run stopped by the team (operational incident). Run 20261108T130803Z_C5_experiment_pro_pro_hard (commit 8f72b02, clean tree, profile experiment_pro, --run-usd 5.00; input sha256 acfd3825…26cf7a66, the 10 hard test problems in dataset order) was stopped on purpose at about 17:23 UTC, together with its whole process tree (REPL, lake), because the team had to leave. No code, prompt, model or configuration changed; all calls were off-peak. 5 of 10 problems finished and are kept unchanged: imo_1965_p2, imo_1993_p5, imo_1979_p1 (failed), imo_1987_p6 (budget_exhausted) and imo_1978_p5 (provider_error: the Autoformalizer request on subgoal 1, the problem's 30th call, got APIConnectionError: Connection error. with no HTTP response on all 5 transport attempts, 15:34:50–15:37:28 UTC). The 6th (imo_1984_p6) was cut mid-problem after 4 calls and left no row. The last 4 (imo_1964_p1_2, putnam_1964_b2, putnam_1995_b1, putnam_1965_b2) were not attempted. The run is not resumed and the provider_error is not re-run: the exploratory table reports the 5 finished rows, the cut problem and the 4 not attempted as such. Real cost 1.9407 USD (151 paid calls; 0.1725 USD of it on the cut problem, in no kept row); ledger total after the run 9.3003 USD. run_config.json still shows status: running because the run never reached its final rewrite.

Clarifications written before any run on test:

2026-11-03, FPR_B check (§4.2), how "the Autoformalizer–Verifier loop with the same budget" is implemented (scripts/run_baseline_b.py --check, baselines/baseline_b.check_claim): each claimed proof (B⁺) is the sketch of the Autoformalizer on the trivial plan (the whole theorem as the only subgoal), with the Retriever's lemmas as in C5; up to critic.k_max = 3 attempts, each failure classified by κ and followed by the Critic's deterministic feedback (no LLM advice, no Planner, no Generator, no automation pre-pass, so no fixed tactic can stand in for the claimed proof); its own budget of B_max = 40 calls, counted apart from C2's own calls (C2's efficiency figures exclude the check; in practice the check makes at most k_max × 2 = 6 calls: one Autoformalizer call and at most one JSON repair per attempt). Acc is Eq. 2 on the assembled theorem. FPR_B = not_verified / (verified + not_verified), where budget_exhausted counts as not_verified (the budget is part of the method). A check that ended in provider_error, budget_stop or error, or a row marked lean_down, is left out of FPR_B, counted apart and re-run once like a provider_error (§5); if it fails again the same way it is reported as not checked. Problems C2 did not claim are not checked.

Analysis plan (pre-registered before any run on test)