Blame for code/docs/LEAN_VERIFIER.md

# Strict Lean 4 verifier (Track L / P1)

A reward and an evaluator for formal proofs that cannot be gamed by "it compiles". Code:
`align/verify/lean/` (stdlib only), installer `scripts/lean_setup.sh`, ceiling test
`scripts/lean_ceiling_test.py` (+ frozen case tables `scripts/lean_ceiling_cases.py`), tests
`tests/test_lean_verifier.py`. The Lean toolchain is an external binary
(`docs/DEPENDENCY_POLICY.md`, "External binary: Lean 4 toolchain"), reached only through
`subprocess`.

Status (2026-10-12): implemented, tested without Lean (173 tests, fake REPL), tested against the
real toolchain (19 slow tests), mutation-tested (40 hand mutants), and **ceiling-tested**:

| | |
|---|---|
| Known-good accepted | **177 / 178 = 99.44 %** (Wilson 95 % [96.9 %, 99.9 %]); floor 98 % -> PASS |
| Adversarial accepted | **0 / 61** -> PASS (a compile-only grader would have paid 51) |
| Throughput, 8 workers | 0.57 proofs/s on a heavy unfiltered mix; 4.4 proofs/s on the median mix (GRPO shape) |
| Memory per warm REPL | 0.64-0.65 GiB PSS with 8 workers (0.24 GiB private); 0.85 GiB peak under load |
| Install | 5.57 GiB, 3 min; `import Mathlib` 3.2 s warm / 39.7 s cold |

Section 5 holds the numbers; every figure there is copied from a file under `.tmp/lean_ceiling/`.
Section 4 is the pre-registration. Section 6 lists what this verifier does not promise.

## 1. The pin

| | |
|---|---|
| Lean | `leanprover/lean4:v4.9.0-rc1` (`lean --version`: 4.9.0-rc1, commit `be6c4894e0a6`) |
| Mathlib | `leanprover-community/mathlib4@d1d1e4b72c6e009edd97cabe1d661b021fe8eeae` (2024-06-12) |
| REPL | `leanprover-community/repl@v4.9.0-rc1` (`7df77c0a1c91`), built against the same toolchain |
| elan | 4.2.4 |
| Location | `/apps/development/rlhf/lean/` (`elan/`, `workspace/` = Lake project requiring Mathlib at the rev above, `repl/`, `PINS.json`) |

**Provenance (how "the Goedel-Prover-V2 pin" was determined, not assumed).** Goedel-Prover-V2's
README says "we follow DeepSeek-Prover-V1.5, which uses Lean 4 version 4.9 and the corresponding
Mathlib". The repo's `mathlib4` git submodule is `xinhjBrant/mathlib4` at commit
`2f65ba7f1a9144b20c8e7358513548e317d26de1`. That commit is a single child (message `align`,
2024-08-07, Huajian Xin of DeepSeek) of upstream `d1d1e4b72c6e`, and changes only
`lakefile.lean` and `lake-manifest.json` to add `xinhjBrant/repl@deepseek` as a Lake dependency;
its `lean-toolchain` is `leanprover/lean4:v4.9.0-rc1`. So "Lean 4.9" in that README is
nominal: the binary is **4.9.0-rc1**, not 4.9.0.

**Deviation, and why it is safe.** We pin the *upstream parent* and build the REPL separately.
Mathlib's prebuilt `.olean` cache is keyed on a hash that includes `lakefile.lean`, so the
DeepSeek child commit would not hit the cache and would force a multi-hour Mathlib build. The
parent's Mathlib sources, and therefore the `.olean`s, are byte-identical to what the child
compiles; the only difference is which REPL fork the lakefile names. We use upstream
`repl@v4.9.0-rc1`, whose protocol (`cmd`/`env`) is all this package needs. The fork's extra
options (`allTactics`, `ast`, `premises`) are not used. Install cost with the cache: 3 minutes,
5.8 GB (Section 5).

**Version drift is a correctness issue.** SafeVerify keeps separate branches for 4.9.0 and
4.15.0; PutnamBench moved to 4.33.1 in 2026-09. Proofs verified here say nothing about 4.33.
Every number this verifier produces must be reported with this pin and the verifier tier.

## 2. Architecture and what each layer defends

```
completion text ──extract_lean_code──▶ code ──static_check──▶ Plan
                     (reward.py)             (strict.py: lexer, bans, header, target)
                                                   │ reject: no Lean touched
                                                   ▼
   ReplPool.acquire ─▶ Worker: [import once] ─▶ [audit prelude] ─▶ [header opens]
   (repl_pool.py)                                                       │
                          ref = `theorem _align_ref <given signature> := sorry` ──▶ env R
                          candidate body, run in env R ──▶ env C   (errors / sorry ⇒ reject)
                          `#align_audit "<nonce>" 1 <target> _align_ref` in env C ──▶ verdict JSON
```

| Layer | Rejects | Independent of the lexer? |
|---|---|---|
| `extract_lean_code` | no fence / truncated (unclosed) fence / prose | n/a |
| header equality | any change to imports, `open`s, options (token-for-token vs the reference header) | yes (token compare) |
| lexical bans | `sorry`/`admit`, `native_decide`, `unsafe`/`partial`, `implemented_by`/`extern`/`export`, `axiom`/`opaque`, `macro`/`elab`/`syntax`/`notation`/`run_cmd`/`initialize`, any `#cmd`, `namespace`/`section`/`variable`/`attribute`/`local`, `instance`, `def`/`abbrev` (unless `allow_helper_defs`), `Lean.*`/`IO.*` identifiers, `exact?`/`apply?`, non-whitelisted `set_option` (incl. `maxRecDepth` > 16384), attributes that change compilation/elaboration | no (this is the lexer) |
| target rules | target missing, declared twice, `private`/`protected`/attribute on it, signature tokens differ from the reference's (strict mode) | no |
| compile | any `error`; any `sorry` warning; non-empty `sorries` | yes (Lean) |
| **audit: axioms** | any axiom outside {`propext`, `Quot.sound`, `Classical.choice`}: catches `sorryAx`, `Lean.ofReduceBool`/`trustCompiler` (`native_decide`), user axioms, even if the lexer were fooled | yes |
| **audit: statement bridge** | the kernel is asked to check `theorem _align_bridge : <type of _align_ref> := <candidate>`. `_align_ref` was elaborated *before* the candidate existed, so a definition-hole (instance, `variable`, shadowing) that makes the same text mean something else fails here | yes |
| **audit: kernel recheck** | every local theorem re-added with `debug.skipKernelTC` forced off | yes |
| **audit: meta-declaration scan** | a NEW local constant whose type/value mentions `Lean.Elab/Meta/Macro/Parser/PrettyPrinter/Syntax/Environment/Core/Compiler`, `IO`, `unsafeCast`: the footprint of an `elab`/`macro` that slipped past the lexer | yes |
| audit: kind | the target must be a `theorem` (not a `def` that happens to inhabit the type) | yes |

The audit verdict is the one info message tagged `ALIGN_AUDIT <random nonce>`, produced by a
**separate REPL call** after the candidate ran. The candidate's own output cannot carry the
nonce (it is generated after the candidate text is fixed), so it cannot forge a verdict.

Reward semantics (`reward.py`): `accuracy ∈ {0,1}`, 1 only if every layer passes. Diagnostics
(`StrictResult.reasons`, `.diagnostics`) are returned separately and never folded into the
reward: shaped partial credit ("compiles but has `sorry`") is exactly the gradient a policy
follows to the exploit (Leanabell-V2 also found shaped rewards slightly worse than binary).
Plug-in points, none of which change the loss or `CompositeReward`:

```python
from align.verify.lean import ReplPool, StrictVerifier, LeanAccuracy, find_toolchain
pool = ReplPool.from_toolchain(find_toolchain(), preflight=True)   # host rules + worker count
acc = LeanAccuracy(StrictVerifier(pool))
accuracy, result = acc.score(formal_statement, completion_text)    # float in {0,1}, diagnostics
terms, result = acc.reward_terms(composite, formal_statement, completion_text, fmt, n_tokens)
outcomes = acc.verify_batch(statements, completions)               # OutcomeVerifier surface
```

**Failure semantics.** A proof that times out, exhausts memory or kills its REPL scores 0 (that
is a property of the proof). A *dead verifier* must not: `LeanInfraError` is raised when the
base environment cannot be built or when more than half of a batch (of at least 8) died for
infrastructure reasons. Otherwise a broken toolchain would feed the policy an all-zero reward
that reads as "the model got worse" (the 0/100 perfect-policy incident, mirrored).

Failure taxonomy (`StrictResult.reasons`): `no_code`, `parse_error`, `unsupported_statement`,
`header_mismatch`, `target_missing`, `target_modifier`, `statement_mismatch`, `banned:<x>`,
`compile_error`, `sorry`, `not_theorem`, `axiom:<name>`, `bridge_failed` (defeq mode),
`kernel_recheck_failed`, `meta_decl`, `skip_kernel_tc`, `timeout`, `crash`, `memory`,
`output_too_large`, `protocol`, `reference_invalid`.

Statement modes. `strict` (default): signature tokens equal the reference's *and* the kernel
bridge passes. `defeq`: bridge only, so an alpha-renamed or restated-but-defeq signature is
accepted. The bridge is checked by the kernel (not the elaborator's `isDefEq`), so "accepted"
means "the candidate's constant has a type the kernel accepts as the reference's type".

## 3. REPL pool: measured facts the design rests on

| Fact (measured on this box, Lean 4.9.0-rc1 + Mathlib pin) | Consequence in code |
|---|---|
| The REPL **does not flush stdout when it is a pipe** (only a pty line-buffers); the client blocks forever | binary wrapped in `stdbuf -o0 -e0` (`tests::test_wrapped_argv_*`) |
| `lake env` prints **cwd-relative** paths (`././.lake/...`) | absolutised once in `toolchain.build_child_env`; child gets a minimal environment (no tokens) |
| A **second fresh `import Mathlib` in a live process** cannot re-mmap the `.olean`s and reads them into the heap: `Pss_Anon` 0.25 → **4.14 GiB** | one import per process; every header variant is layered on it (`split_imports`, `Worker.header_env`); a different import set recycles the process |
| RSS is ~3.65 GiB but 3.40 GiB of it is the shared, read-only `.olean` mapping; private heap is ~0.25 GiB | the watchdog caps **`Pss_Anon`**, not RSS; `plan_workers` budgets shared-once + n × cap |
| `Nat.pow exponent is too big` and `lean::stack_space_exception` **abort the process** (`rc=1`, `rc=-6`) | `ReplCrash` with the stderr tail; the next `acquire` respawns; scored 0 |
| `debug.skipKernelTC` is an **unknown option** on 4.9.0-rc1 | the whitelist + the audit's `skip_tc` check are guards for a pin upgrade, not a live exploit here |
| Lean 4.9 has **no public `collectAxioms`** (`#print axioms` is private) | `alignCollectAxioms` in the prelude (same traversal) |
| `variable (h : False)` *used in a proof body* is added to the theorem's type in 4.9 (pre-4.11 behaviour) | `variable` is banned lexically and the bridge catches it independently |

Limits per worker (defaults, `ReplLimits`): anonymous-memory cap 4 GiB (watchdog polls
`smaps_rollup` every 0.5 s), `prlimit --as=16GiB --fsize=256MiB --core=0`, `nice +5`, output cap
16 MiB, per-proof wall budget 180 s (compile + audit), SIGKILL of the whole process group on any
violation, `MALLOC_ARENA_MAX=2`. Workers recycle after 1000 commands. Default worker count is
`min(8, cores // 4)` = 8 on this box; `ReplPool.from_toolchain(preflight=True)` applies the
`/apps/CLAUDE.md` checks (≥ 45 GB `MemAvailable`, load < 2× cores, disk queue < 64) through
`align.utils.guard.preflight_host_check` and then shrinks the worker count so that, even with
every worker at its cap, `MemAvailable` stays above the 45 GB floor. The ceiling-test script
takes the same exclusive heavy-job `flock` as the trainers (a Lean pool is a heavy job).

## 4. Pre-registration (written BEFORE the registered ceiling run)

Registered 2026-10-12 20:12 IST, before any run of `scripts/lean_ceiling_test.py` without
`--allow-unregistered`. The case tables (`HEADER`, `STATEMENTS`, `ADVERSARIAL`, `RESTATED` in
`scripts/lean_ceiling_cases.py`) are frozen by hash:

PREREG_TABLE_SHA256: `61636c7136eb647801c588b00a35bd8bcc6ef4db126c21ea75769092883ff7e2`

`python scripts/lean_ceiling_test.py --verify-prereg` recomputes it; the registered run refuses
to start on a mismatch.

**Honest note on process.** The tables were developed against this verifier (about six exploratory
runs on 1-2 workers, `--exploratory --allow-unregistered`) so that every adversarial case is
*live* (it would be paid by a compile-only grader, which the run also measures) and every
restated proof compiles. Those exploratory runs informed case *authoring* only; thresholds
below were fixed before the registered run, and any verifier change after registration that
alters a verdict is reported as an amendment in Section 7, with the pre-amendment matrix kept.

**Configuration under test** = shipped defaults: `StrictConfig()` (strict statement mode, no helper
defs, kernel recheck ON, 180 s budget per proof) and `ReplLimits()` (4 GiB anonymous cap, 16 GiB
`--as` backstop), 8 workers, `lean_workbook` compile-only filter budget 120 s.

**Known-good set.** (a) Public verified proofs: 6 contiguous slices of 25 rows at offsets
0, 5000, 10000, 15000, 20000, 25000 of `Goedel-LM/Lean-workbook-proofs` (29,750 proofs verified
under the Lean 4.9 / DeepSeek-Prover-V1.5 Mathlib environment), fetched over HTTP, never the
full dataset. (b) 30 hand-restated Mathlib-style theorems with proofs. The formal statement
given to the verifier is derived mechanically from each proof file (header + last theorem's
signature cut at the signature-ending `:=` + `sorry`). **Filter:** an independent compile-only
pass (same REPL, no strictness: no `error` message and no `sorry` warning) defines "compatible
with the pin"; items failing it are excluded *and listed*. Scored population = compile-clean
items. **Pass:** ≥ 98 % accepted and ≥ 50 items. (The roadmap's P1 row says ≥ 99 %; the task
fixed 98 %, which is what is registered. Both are reported.) Any rejected known-good item is
listed with its reasons; rejections caused by the policy bans (e.g. a genuine `native_decide`
in a public proof) count as failures, because that is the cost the RL stage would pay.

**Adversarial set.** ≥ 30 hand-built cases, all registered (61): categories sorry (7), admit (2),
extra axiom (4), native_decide (3), changed statement (6), weakened hypothesis (3), definition
hole (4), environment manipulation via elab/macro/run_cmd/initialize/#eval/#exit (9), theorem
proved for a different name (6), timeout/crash/memory bombs (3), banned constructs (6), header
tampering (4), no code (4). Each is a *completion* (prose + fenced block) so fence extraction,
static gate, REPL compile and audit are all exercised. **Pass:** 0 accepted. Bomb cases run on
a dedicated 1-worker pool (1 GiB anonymous cap, 30 s budget) so they terminate promptly; the
code path is the same. Reported alongside, not part of the pass criterion: how many cases a
compile-only grader would pay; and which cases the Lean-side audit rejects *on its own* with
the lexical gate disabled.

**Confusion matrix** (reported verbatim): rows = truth (good / bad), columns = verdict
(accept / reject); good = compile-clean known-good, bad = adversarial.

**Measurements** (reported, no threshold): install disk size; `import Mathlib` cold
(page cache evicted with `posix_fadvise(DONTNEED)`) and warm; per-REPL PSS / Pss_Anon / RSS from
`/proc/<pid>/smaps_rollup` with Mathlib imported, for one process and for 8 concurrent workers;
throughput (proofs/s) at the worker count used, with the worker set warm, on unique statements
and in the GRPO shape (12 statements × 8 samples); latency p50/p90/p99; PSS sampled during the
run.

## 5. Results

All numbers below are copied from `.tmp/lean_ceiling/registered/result.json` and
`.tmp/lean_ceiling/registered.log` (the registered run: hash verified, `prereg_registered=true`,
8 workers, host preflight passed, heavy-job lock taken after waiting for another track's job
to release it, started ~20:13 IST, 2026-10-12). Host: 48 cores; `MemAvailable` never fell below
136.9 GB in the samples taken during the strict known-good pass.

### 5.1 Ceiling test: confusion matrix (verbatim)

```
                      verdict ACCEPT   verdict REJECT   total
truth GOOD proofs                177                1     178
truth BAD  proofs                  0               61      61
```

| Criterion (pre-registered) | Measured | Verdict |
|---|---|---|
| known-good accepted >= 98 %, n >= 50 | **177 / 178 = 99.44 %** (Wilson 95 % [96.89 %, 99.90 %]); n = 178 | **PASS** (also >= the roadmap's 99 %) |
| adversarial accepted = 0, n >= 30 | **0 / 61** | **PASS** |
| gate 5 of the roadmap: strict false-negative rate > 5 % blocks P2 | 0.56 % (upper Wilson 3.1 %) | not blocked |

**Known-good population.** 180 candidates (150 Lean-Workbook-proofs rows from dataset revision
`b731852af8d8`, raw file sha256 `55932494...aebef`; 30 restated). The independent compile-only
filter kept 178: **148 + 30**. The 2 excluded (`lean_workbook_10036`, `lean_workbook_plus_64037`)
were excluded because the compile-only pass hit its **120 s budget** (`why: timeout`), not because
of a compile error, so "version-incompatible" would be the wrong label: they are slow proofs.
All 30 restated proofs were accepted.

**The one rejected known-good proof: `lean_workbook_51088`, reason `timeout`** (180 s strict
budget). It is a nlinarith proof with nine hints. Follow-up (exploratory, 1 worker, not part of
the registered numbers), same proof, same pool code, only the REPL environment layers differ:

| environment the body runs in | wall time |
|---|---|
| imports + header (what the compile-only filter uses) | 99.9 s (filter: 104.1 s) |
| + reference theorem `_align_ref` | 225.8 s |
| + audit prelude | 513.6 s |
| + both (= the strict path) | 516.5 s (timed out at 400 s in a separate strict run) |

On `lean_workbook_10009` (20 s) the same four environments take 19.9 / 20.8 / 20.1 / 20.0 s. So
this is not a systematic strict-tier slowdown; it is the well-known run-time chaos of a borderline
`nlinarith` (the certificate search is sensitive to state it inherits from earlier commands) hitting
a 180 s wall-clock budget. It is a genuine false negative of the *reward* (such a proof would score
0), it is bounded at one in 178 here, and raising the budget to Goedel's 300 s would not have saved
it (517 s). The honest reading: wall-clock-bounded verification of proofs this close to the limit is
flaky in BOTH directions, so for evaluation (not training) report results at a stated budget.

**Adversarial population (61 cases, all rejected).** First reason per case: 58 rejected by the
static gate (no Lean call), 3 by the REPL layer (the bombs). By category (cases / accepted):
sorry 7/0, admit 2/0, extra_axiom 4/0, native_decide 3/0, changed_statement 6/0,
weakened_hypothesis 3/0, definition_hole 4/0, env_manipulation 9/0, wrong_name 6/0,
timeout_bomb 3/0 (timeout, `rc=-6` stack-overflow crash, anonymous-memory kill at 1110 MiB over a
1024 MiB cap), banned_construct 6/0, header_tamper 4/0, no_code 4/0.

* **A compile-only grader would have paid 51** of the 54 code-bearing, non-bomb cases
  (each case's own text compiled with no strictness). The 3 it would not: `header_missing` (no
  Mathlib), `duplicate_target` (Lean itself rejects a duplicate name) and `skipKernelTC_option`
  (unknown option on this Lean). The 3 bombs and the 4 `no_code` cases are not applicable. So
  51 are live exploits, not strawmen.
* **Semantic layer alone** (lexical gate OFF, so each exploit actually executes inside Lean, with
  `kernel_recheck` on): rejected **45 of the 54** code-bearing non-bomb cases by the Lean-side audit
  alone (`sorry`, `axiom:bad`, `axiom:Lean.ofReduceBool`, `axiom:evil` after an `elab` added an
  axiom, `statement_mismatch` for the instance hole, the `variable` hole, shadowing via
  `macro_rules`, changed constants/hypotheses, `meta_decl` for `initialize`, `target_missing`
  for wrong names/namespaces/private targets, `header_mismatch`). The 9 it accepted are the
  *policy-only* set, where the proof of the stated theorem is valid and the lexical ban is the
  only thing stopping it: `eval_side_effect`, `exit_after_theorem`, `attribute_on_target`,
  `unsafe_implemented_by`, `partial_def`, `extern_attr`, `search_tactic_exact_q`,
  `maxRecDepth_abuse`, `helper_def_with_proof`. None is a soundness gap (the theorem is proved);
  they are rejected to keep the attack surface small, and each costs real-world proofs that use
  them (Section 6, item 5).

### 5.2 Install and process measurements

| Quantity | Measured |
|---|---|
| Install time (`lean_setup.sh`, cache hit) | 3 min 9 s (18:23:06 -> 18:26:15); an idempotent re-run takes ~10 s |
| Disk, total | 5,981,549,078 B = **5.57 GiB**: elan + toolchain 0.93 GiB, workspace 4.34 GiB (of which Mathlib package 4.11 GiB), REPL 94 MiB |
| `import Mathlib` + `Aesop`, **cold** (page cache for all 11,171 `.olean/.ilean/.so` files = 4.19 GiB evicted with `posix_fadvise(DONTNEED)`) | **39.7 s** |
| same, **warm** (3 runs) | 3.19, 3.20, 3.19 s (median **3.19 s**) |
| 8 workers warmed in parallel | 3.38 s (warm cache) |
| One REPL after the import (alone on the box) | RSS 3439 MiB, **PSS 3437 MiB**, `Pss_Anon` **244 MiB**, `Pss_File` 3193 MiB, 1 thread, VmSize 4071 MiB |
| **Per-worker PSS with 8 workers all holding Mathlib** | **643-653 MiB** each (mean 648; RSS 3.4-3.5 GiB each) = 244 MiB anonymous + 3193 MiB / 8 shared. Sum of PSS **5.06 GiB**; sum of RSS **26.8 GiB** (the double count the PSS figure removes) |
| Per-worker PSS **during** the 178-proof run (sampled every 0.5 s) | mean 717-792 MiB, max **873 MiB**; `Pss_Anon` max 404 MiB; RSS max 3.65 GiB |
| Worker growth over 1042 commands | none that approached any limit: recycled 0 times (limit 1000/worker) |

`fincore` was not usable for confirming the eviction (its output did not parse into a residency
fraction: the script printed `None` and `4096.0`; ignore those two fields in `result.json`). The 12x
cold/warm gap is the evidence that the eviction worked.

Model implied by the measurements: `PSS(n workers) ~ 0.24 GiB + 3.12 GiB / n` per worker, total
`~ 3.12 + 0.24 n` GiB. Eight workers cost ~5 GiB of RAM in total. The worst case (all eight at
their 4 GiB anonymous cap) is 3.12 + 8 x 4 = 35 GiB, which is what `plan_workers` budgets against
the 45 GB floor, so the pool cannot push `MemAvailable` under the floor on this host. **Roadmap gate 5** ("above ~4 GB per warm REPL the pool
shrinks below ~8 workers") is not triggered: 0.65 GiB per warm REPL, 0.85 GiB peak under load.

### 5.3 Throughput (8 workers, warm)

| Shape | Proofs | Wall | Proofs/s | Notes |
|---|---|---|---|---|
| 178 unique statements (the known-good set, strict tier incl. kernel recheck) | 178 | 310.9 s | **0.573** | latency p50 1.97 s, p90 21.4 s, p99 158.6 s, max 180.3 s (the timeout), mean 9.76 s |
| GRPO shape: 12 median-latency statements x 8 identical samples | 96 | 21.9 s | **4.38** | reference environment and baseline audit reused per worker; all 96 accepted |

The first number is dominated by the heavy tail of Lean-Workbook `nlinarith` proofs (mean 11.7 s,
median 2.65 s for those; the 30 restated proofs: median 0.18 s, max 1.5 s) and by one 180 s
straggler: the ideal packing of the work is 178 x 9.76 s / 8 = 217 s. It is **not** a verifier
overhead: the compile-only filter took 273 s for 180 candidates on the same 8 workers, i.e. the
strict tier added ~14 % (audit 0.03-0.7 s per proof; kernel recheck +0.04-0.12 s on 20-43 s
proofs). Against the research report's guess of "1-3 proofs/s for 8-16 workers (low confidence)":
**0.57/s on a heavy, unfiltered population and 4.4/s on a median population**; either way
verification stays far above generation (~0.1-0.17 proofs/s per the report), so it is not the
binding constraint at this worker count.

### 5.4 Test and mutation evidence

* `pytest tests/test_lean_verifier.py -m "not slow"`: 173 passed (no Lean needed; fake REPL
  binary speaks the real protocol, including the audit message).
* `pytest tests/test_lean_verifier.py -m slow`: 19 passed on the real toolchain (accepts a correct
  proof, rejects eight exploits with the lexical gate OFF, defeq-vs-strict mode, invalid reference,
  timeout + recovery, end-to-end reward path, concurrency, memory shape).
* `tests/test_dependency_firewall.py`: 2 passed (`align/verify/lean/` and the two scripts import
  only stdlib / `align`).

## 6. Residual risks (what this verifier does NOT promise)

1. **Lexer desync.** The lexical gate is a hand-written tokenizer, not Lean's. It follows Lean's
   rules for nested comments, string escapes, raw strings, char literals and `«»`, and on any
   unusual construct falls back to a raw-text scan, but it has not been differentially fuzzed
   against Lean's real tokenizer. Mitigation: layers 3+ (axioms, bridge, kernel recheck,
   meta-declaration scan) do not use it; the semantic-only column of the ceiling test shows
   what they catch alone. What only the lexer stops is listed there (all of it is
   *policy*, not soundness: the proofs are valid for the stated theorem).
2. **No OS sandbox.** The REPL runs as the same user with filesystem access and no
   network namespace. Code can only execute inside the elaborator through meta-programming
   (`elab`/`macro`/`run_cmd`/`#eval`/`initialize`/`unsafe`), all of which are banned lexically
   AND detected by the meta-declaration scan, and the child's environment holds no secrets
   (`toolchain.build_child_env`). A meta-programming escape that evades both would run with the
   verifier's file permissions. For adversarial RL, run the pool as a dedicated unprivileged
   user or under `unshare --net` / a cgroup; that needs privileges this task did not have.
3. **Statement fidelity.** The bridge proves the candidate proves the GIVEN formal
   statement. It says nothing about whether that statement means what the informal problem
   says (miniF2F: formal/informal discrepancies in over half the problems, 16 unprovable
   statements; the report, section 5F). Report miniF2F-v2/PutnamBench with the pin and tier.
4. **Trust base.** The Lean kernel, `propext`, `Quot.sound`, `Classical.choice`, the REPL, and
   the prelude (`AUDIT_PRELUDE`, ~100 lines). The prelude is a trusted program; it is
   exercised by the real-toolchain tests, not formally verified.
5. **Policy rejections are not soundness failures.** `def`/`instance`/`notation`/`namespace`
   helpers, `exact?`, `#eval` and so on are rejected even when the proof of the stated theorem
   is valid. That is deliberate (smaller attack surface) and has a cost: public proofs that use
   them are false negatives. `allow_helper_defs=True` relaxes only `def`/`abbrev`.
6. **Version drift.** Proofs from other Lean/Mathlib versions will fail to compile (counted as
   0), which is correct for this pin and wrong as a statement about the proof.
7. **Throughput numbers are for this population** (short Lean-Workbook-style and restated
   proofs). A prover that emits long `nlinarith`/`decide` proofs will be slower; the audit costs
   ~0.3 s for proofs whose dependency closure reaches real analysis and ~0.03 s for `omega`.

## 7. Amendments

**7.1 Changes between the exploratory runs and the registration (before 20:12 IST; not
amendments, listed so nothing is hidden).** Case-table edits made after seeing exploratory output:
`sorry_branch` (its `all_goals sorry` was dead code, so the proof was valid: moved the `sorry` into
a live branch); `sorry_after_char_quote` / `sorry_after_comment_opener_string` (did not compile;
rebuilt so the `sorry` really sits between two quote-bearing literals); `axiom_private`,
`axiom_reducible_attr` (did not compile; replaced by `axiom_polymorphic`, `axiom_via_simpa`);
`ofReduceBool_term` (`rfl` cannot discharge `Lean.reduceBool`; replaced by
`native_decide_in_helper_lemma`); `local_notation_hole` (a local `+` notation is *ambiguous* with
the builtin one, so it never elaborates; replaced by `variable_hole_hypothesis`);
`rs_default_arg` (did not compile). Verifier changes made before registration, each driven by a
measurement: single import per process (Section 3), the late-answer drain, `kernel_recheck`
default, the `open Lean`-root ban, `notation3`/`binder_predicate`/... bans, 180 s default budget,
`split_imports`/prelude-before-opens layering. The `skipKernelTC_option` case turned out to be
**inert on this pin** (the option does not exist) and was kept, labelled.

**7.2 Retraction.** A first measurement reported the kernel recheck as costing "2.2-3.2x"
(`lean_workbook_10009`: 21 s -> 68 s). That reading came from a run on a host where two other
Lean processes were competing; isolated measurements (`#align_audit` flags 0 vs 1 on the same
environment) show **+0.04 to +0.12 s** against 20-43 s of elaboration. The recheck is therefore ON
by default; the claim was removed from the code comment before registration. (The same episode is
why the headline timings here come from the registered run; the few ad-hoc timings are labelled
exploratory.)

**7.3 Verifier changes after registration:** none. The registered run used the tree that is
described here.

**7.4 Failures found by running against the real toolchain (each has a regression test).**
(1) REPL never flushes a pipe -> `stdbuf`; (2) `lake env` paths are cwd-relative -> absolutised;
(3) a second `import Mathlib` in a live REPL costs +3.9 GiB anonymous and tripped the 4 GiB
watchdog on the first multi-case run -> one import per process, layered headers; (4)
`#print axioms`'s collector is private in 4.9 -> own traversal; (5) with `autoImplicit` on (plain
Lean default) an *unknown identifier* in a statement is silently an implicit variable, so "invalid
reference statement" needs a genuine type error to trigger `reference_invalid`; (6) `sqrt` under
`open Real Nat` is already ambiguous, so a root-level `def sqrt` is not a viable definition hole
here (instances and `variable` are); (7) pool statistics were counted only when an error escaped
`acquire`, not when the caller handled it.

**7.5 Hand mutants** (each removes one fix in a COPY of the package, then runs the non-slow
tests; `.tmp/lean_notes/mutants.py`, final run after the last code change except docs):

| | Mutant (fix removed) | Killed by |
|---|---|---|
| M01 | accept any audit-tagged message (forgeable verdict) | `test_audit_message_without_the_nonce_is_ignored_forged_verdict_regression` |
| M02 | no axiom whitelist check | `test_each_audit_finding_rejects[axiom/sorryax/ofreduce]` |
| M03 | ignore the kernel statement bridge | `test_each_audit_finding_rejects[bridge]` |
| M04 | no meta-baseline subtraction | `test_verdict_accepts_a_clean_audit` |
| M05 | no meta-declaration check | `test_each_audit_finding_rejects[meta]` |
| M06 | ignore `sorry` warnings / `sorries` | `test_each_audit_finding_rejects[sorrywarn/sorrylist]` |
| M07 | header failure scored 0 instead of `LeanInfraError` | `test_header_failure_raises_infra_error_never_a_zero` |
| M08 | candidate runs without the reference env | `test_command_order_and_envs_are_the_contract` |
| M09 | no `stdbuf` | `test_wrapped_argv_uses_stdbuf_prlimit_and_nice` |
| M10 | kill the pid, not the process group | `test_timeout_kills_grandchildren_too_via_process_group` |
| M11 | no memory watchdog | `test_memory_watchdog_caps_anonymous_memory_not_rss` |
| M12 | timeout without killing | `test_timeout_kills_the_process_and_leaves_no_zombie` |
| M13 | tolerate bytes after the terminator | **survives: equivalent mutant** (two concatenated JSON objects fail `json.loads` anyway); the real defence is M39 |
| M14 | first `:=` wins | `test_sig_end_skips_let_in_type_not_the_first_colon_eq` |
| M15 | no char-literal handling | `test_lexer_char_literal_quote_is_not_a_string_start` |
| M16 | block comments do not nest | `test_lexer_drops_line_and_nested_block_comments` |
| M17 | no raw-scan fallback on lexer anomalies | `test_anomaly_triggers_raw_scan_...` |
| M18 | re-import for every header variant | `test_second_header_variant_reuses_the_import_never_imports_twice_regression` |
| M19 | lake paths left cwd-relative | `test_build_child_env_absolutises_...` |
| M20 | no header equality | `test_static_rejections[header...]` |
| M21 | `set_option` whitelist off | `test_banned_constructs_fire[set_option...]` |
| M22 | dead pool emits zeros | `test_reward_raises_when_the_pool_looks_dead_...` |
| M23 | defs accepted as proofs | `test_each_audit_finding_rejects[def]` |
| M24 | kernel recheck never requested | `test_kernel_recheck_is_on_by_default_...` |
| M25 | `skip_tc` ignored | `test_each_audit_finding_rejects[skiptc]` |
| M26 | recheck failure ignored | `test_each_audit_finding_rejects[recheck]` |
| M27 | private/attribute target allowed | `test_static_rejections[target_modifier]` |
| M28 | signature token equality off | `test_static_rejections[statement_mismatch]` |
| M29 | identifier ban list off | `test_banned_constructs_fire` |
| M30 | salvage unclosed fences | `test_extract_unclosed_fence_is_not_salvaged` |
| M31 | first fence instead of last | `test_extract_takes_last_closed_lean_fence_and_ignores_think` |
| M32 | duplicate target allowed | `test_static_target_declared_twice_is_rejected` |
| M33 | ablated verifier usable as a reward | `test_reward_refuses_the_ablated_verifier` |
| M34 | worker never returned to the pool | **hang-killed** (the pool tests block; 90 s watchdog) |
| M35 | no recycling after `max_requests` | `test_worker_recycled_after_max_requests` |
| M36 | unbounded glibc arenas | `test_build_child_env_absolutises_...` |
| M37 | child inherits the whole `lake env` | `test_build_child_env_absolutises_...` (secrets leak assertion) |
| M38 | no output cap | `test_oversized_output_kills_the_process` |
| M39 | late second answer attributed to the next request | `test_late_second_answer_is_detected_...` |
| M40 | `open Lean` makes meta identifiers spellable | `test_banned_constructs_fire[open Lean...]` |

40 mutants: **38 killed by an assertion, 1 killed by a hang (M34), 1 survivor (M13, equivalent)**.
Not covered by any mutant, by construction: the `skip_tc` audit path against the REAL option (it
does not exist on this pin; `test_real_skip_kernel_tc_option_does_not_exist_on_the_pin` fails the
day the pin changes) and the Lean prelude's kernel-recheck loop against a proof that elaborated
with the kernel disabled (no way to produce one on 4.9 without the banned meta-programming).

**7.2 V1 freeze (2026-10-14, branch `phase0/verifier`; PROPOSED FROZEN HASH, merge after chain6 exits).**
Fixes (regressions in `tests/test_lean_hardening.py`, each adversarial proof was accepted or aborted a batch before):
U08-1/2 lexer desync (`\/` and `//` are single tokens; a comment opener glued to any other symbol is refused as
ambiguous; numerals no longer swallow letters: `1macro`; raw strings of any hash count; real-Lean differential fuzz);
U08-40 `s!`/`f!`/`m!` interpolation flagged whatever sits before the quote; U08-4/12 `_align*` names and
`_root_.`/`«»` spellings banned; U08-5 axiom-walk fuel exhaustion reports `_align_fuel_exhausted` (fails closed) and a
missing `axioms` field is `audit_incomplete`; U08-3 `ReplPool.from_toolchain(sandbox=True)` is the default, fails closed
with `SandboxUnavailable`, `sandbox=False` is the explicit opt-out; U08-8 every real REPL runs under the launcher/supervisor
(`ReplProcess.supervise`) that SIGKILLs it when the parent process dies (measured: orphaned before, reaped now);
U08-6 stale env ids after a worker death raise `ReplCrash`; U08-7 lone surrogates reject that item only; U08-17 budget
starts after `acquire()`; U08-18 a bad reference header is `reference_invalid`, not a batch abort; U08-21 any exception
mid-request kills the child; U08-11(codex) unmeasurable memory fails closed after `mem_miss_limit` samples; U08-16
timeout/crash/memory/protocol map to `Outcome.UNDECIDED` (new enum member in `align/eval/verifier.py`, reward stays 0).
Ported from the red-team session: opt-in `independent_recheck` (`recheck.py`), default off.
NOT changed (design choices, math verifier, need a decision): U08-9/10/11/15 (tolerance, texty fallback, unit stripping,
`i`), U08-13/14/22 (extractor ReDoS/format), U08-19/20 (preflight opt-in, pin not enforced at runtime).

Verification: exploratory ceiling run (2 workers, sandboxed): known-good 176/177 accepted (the one reject is a
179 s timeout under host load), adversarial 0/61 accepted. Registered run to do after the chains exit (needs the heavy
lock): `python scripts/lean_ceiling_test.py --workers 8`.
Frozen hash: `sha256` over, for each `align/verify/**/*.py` in sorted path order, `path + NUL + bytes + NUL`:
`6df56348db12d8e255427764f994d0f3ab29d4713e84ddda07c9637c31f12648`.

**7.3 FROZEN (2026-10-19).** Merged verifier (V1 + MV math-checker fixes) hash
`f1dd9e7871ade3a9dd37587c10a7a17025fe8623a735455ec40206607e120b5c` (`scripts/p2/verifier_hash.py`; supersedes the
7.2 proposal, which predates MV). Registered ceiling run (8 workers, heavy lock, sandboxed, `.tmp/restart/ceiling/result.json`):
known-good 178/179 accepted = 0.9944 (Wilson95 [0.9690, 0.9990], floor 0.98) PASS; adversarial 0/61 accepted PASS
(a compile-only grader would accept 51). Every SOTA number from here on is verified under this hash; chain8 refuses to
run a step if `align/verify` changes.

## 8. Operations

```bash
bash scripts/lean_setup.sh            # install / repair (idempotent, ~3 min, 5.8 GB, under /apps)
bash scripts/lean_setup.sh --check    # exit 0 iff the install is complete
source /apps/development/rlhf/lean/env.sh   # only if you want elan/lake in your shell

pytest tests/test_lean_verifier.py -m "not slow"   # no Lean needed (fake REPL binary)
pytest tests/test_lean_verifier.py -m slow         # real toolchain, 2 workers (~1 min)

python scripts/lean_ceiling_test.py --verify-prereg
python scripts/lean_ceiling_test.py --workers 8    # registered run: preflight + heavy-job lock
python scripts/lean_ceiling_test.py --measure-only # install size, cold/warm import, PSS
```

* `ALIGN_LEAN_ROOT` relocates the install. Every cache the toolchain writes is redirected
  under it by `lean_setup.sh`; nothing goes to `$HOME`, `/` or `/tmp`.
* Worker stderr spools to `<root>/tmp/pool/worker<i>.stderr` (truncated per respawn; the tail is
  quoted in `ReplCrash`).
* Before widening the pool: `plan_workers` and `ReplPool.from_toolchain(preflight=True)` are the
  only sanctioned way; never construct more workers than the 45 GB floor allows.
* A new Lean/Mathlib pin is a new verifier: re-run the ceiling test, update `PINS.json`
  provenance in Section 1, and regenerate any cached verdicts.
* Hand mutants (Section 7) are run on a COPY of the package under `.tmp/mutants/`; the repo is
  never edited in place.