> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Re-check proofs

> Check a release's proofs with stock Lean 4 and Mathlib, without any theformalera code.

Every PASS is a Lean 4 file. You can check it with the same toolchain that checked it in the first place, independently of the engine, the Hub and us.

## The easy way

```bash theme={"system"}
theformalera cert verify release.cert.json --require L1 --pubkey release.pub --proofs
```

With `--proofs`, `cert verify` checks every proof file's digest against the certificate. It then compiles the lemma closure (`proofs/lemmas/`) from source into a scratch directory, and runs `lake env lean` on every proof in the locked spec workspace.

## By hand, with stock Lean

You need the spec package the certificate pins (`predicate.spec_digest`), built with `lake build`, and the release directory (`release.cert.json`, `proofs/`, `proofs/lemmas/`).

```bash recheck.sh theme={"system"}
#!/usr/bin/env bash
# Re-check a release's proofs with the standard Lean 4 toolchain only (no theformalera code).
set -euo pipefail
REL=$PWD
SPEC=/path/to/the/locked/spec/package/lean     # its digest is pinned by the certificate
OUT=$(mktemp -d)
cd "$SPEC"

# 1. the lemma dependency closure, compiled from the shipped Lean source
for f in $REL/proofs/lemmas/TFELemmas/*.lean; do
  m=$(basename "$f" .lean)
  mkdir -p $OUT/TFELemmas
  lake env lean --root=$REL/proofs/lemmas "$f" -o $OUT/TFELemmas/$m.olean
done
export LEAN_PATH=$OUT

# 2. every proof, with `#print axioms` of its main theorem appended
for f in $REL/proofs/*.lean; do
  ns=$(grep -m1 '^namespace' "$f" | cut -d' ' -f2)
  { cat "$f"; echo "#print axioms $ns.implements"; } > $OUT/check.lean
  echo "== $(basename "$f")"
  lake env lean $OUT/check.lean | grep -E "error|axioms" || true
done
```

A real run on a release of the example repository:

```text theme={"system"}
$ grep -c sorry proofs/*.lean proofs/lemmas/TFELemmas/*.lean | awk -F: '{s+=$2} END {print NR " files, " s " occurrences of sorry"}'
9 files, 0 occurrences of sorry
$ time ./recheck.sh
lemma closure compiled from source: TFELemmas.Pack_2f5f29ad9072
== rmsnorm_kernel__layers____input_norm__9d6f70d2a5.lean
'TFE.Cert.rmsnorm_kernel_input_norm_4ea45477.implements' depends on axioms: [propext, Classical.choice, Quot.sound]
== silu_mul_tanh_kernel__layers____mlp_act__156cd7f53b.lean
'TFE.Cert.silu_mul_tanh_kernel_mlp_act_f9d7de5b.implements' depends on axioms: [propext, Classical.choice, Quot.sound]

real	0m7.989s
```

![Terminal: recheck.sh compiles the lemma closure and checks two proofs; each depends only on propext, Classical.choice and Quot.sound](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/screenshot3-independent-lean-recheck.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=14a7807e7d71a467450381606b523a40)

## What to look for

* Lean must accept every file with no errors.
* `#print axioms` of each `implements` theorem must list **only** `propext`, `Classical.choice` and `Quot.sound`. Any other axiom (`sorryAx`, a custom axiom, `Lean.ofReduceBool` from `native_decide`) means the proof does not count.
* The theorem's statement is `Implements … (spec)` for the Op Spec of the node in the certificate. Read the certificate's header: it names the kernel and the Spec Key.

## Reading a proof file

A proof file is self-contained apart from the spec library and the lemma closure. In order, it contains:

1. `Args`: the kernel's global memory per pointer argument, and its scalar arguments;
2. one definition per Triton IR value, documented with the IR line and source location (`norm.py:16`);
3. the binding hypotheses `Hyp`: the layouts of your tensors, the scalars, and that outputs do not overlap inputs;
4. the theorem `implements`, and its proof.

The proof's value subgoals end in `tfe_close` or `tfe_replay "<tactic script>"`. When a lemma was hit, its module is imported from the closure.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.