How to Audit a Lean 4 Formalization: Escape Hatches, Axioms, and Specification Seams

A practical checklist for auditing a Lean 4 proof repository: checking axioms, catching native_decide and implemented_by, replaying with leanchecker --fresh and nanoda, and testing specification seams.

1. Why lake build exiting 0 is only the start

When lake build exits with code 0 on a Lean 4 repository, you know only that the elaborator and kernel accepted the files that were built. It does not tell you whether sorry warnings were ignored, whether custom axioms or compiler-trust primitives (Lean.ofReduceBool) were introduced, whether prebuilt .olean caches were trusted without fresh environment checking, or whether the theorem statement actually expresses the informal claim.

An audit separates two questions: **(a) Is the proof sound in Lean’s logic?** (decided by kernels and environment checkers) and **(b) Does the formal statement mean what the paper or specification claims?** (the specification seam, tested by reading custom definitions, proving Mathlib bridges, and running planted wrong variants).

2. Check the axiom footprint of every main theorem

In standard Mathlib developments, a theorem should depend on at most the three classical axioms: propext (propositional extensionality), Classical.choice (the axiom of choice), and Quot.sound (quotient soundness). Constructive theorems may depend on none.

Append #print axioms for every headline theorem in a scratch file or at the bottom of the challenge file:

#print axioms MainTheorem
-- Expected output:
-- 'MainTheorem' depends on axioms: [propext, Classical.choice, Quot.sound]

3. Scan for escape hatches and environment manipulation

A proof that avoids sorry in the main file can still bypass the kernel in five ways:

1. **Custom axiom or opaque declarations:** Any axiom in an imported project file appears in #print axioms, whereas an opaque constant has no unfoldable body, meaning theorems about it only hold for an unspecified inhabitant.

2. **native_decide and Lean.ofReduceBool:** Proves a decidable proposition by executing compiled native code rather than kernel reduction. If any reachable function carries @[implemented_by] or @[extern], the compiled binary runs different code from the logical definition.

3. **set_option debug.skipKernelTC true:** Disables kernel type checking entirely in the current scope.

4. **#exit mid-file:** Stops elaboration at that line with exit code 0; any theorem below #exit was never checked.

5. **Elaboration-time metaprogramming (#eval, run_cmd, elab, macro):** Can mutate the Lean environment or redefine notation so a statement looks like textbook notation while unfolding to a trivial proposition.

4. Replay from scratch with leanchecker --fresh and nanoda

Because .olean files can be modified on disk or polluted by metaprograms, an high-assurance audit replays exported declarations from the root theorem:

• **leanchecker --fresh <Module>** replays kernel type checking from the theorem’s transitive dependencies without trusting cached .olean state.

• **[Comparator](https://github.com/leanprover/comparator) with enable_nanoda: true** exports the kernel environment and checks it with both Lean’s reference kernel and nanoda, an independent Rust kernel implementation, verifying that the proved statement matches the challenge file and uses only permitted axioms.

Note that full Mathlib-scale replays are memory-intensive: on the October 2026 ETH formalizations, Comparator peaked at 80 GiB of RAM for OpenAI’s repository and 24 GiB for Anthropic’s.

5. Close the specification seam: custom definitions and planted wrong variants

Once the kernels agree that the proof proves the statement, the remaining risk is entirely in the **statement file**:

• **Inventory every custom definition:** List every def, abbrev, structure, inductive, and instance reachable from the theorem’s signature. Compare each against the standard Mathlib definition or prove a bridge lemma between them.

• **Prove a consistency witness:** Exhibit concrete inputs satisfying all hypotheses simultaneously so the theorem cannot hold vacuously.

• **Compile planted wrong variants (Mutants.lean):** Replace the conclusion with False (vacuity probe), perturb numeric constants (32 → 31), and tighten relations (≤ → <, = → ≠). Every wrong variant must fail to compile.

Questions & Answers

Sources & References

1. Lean FRO — Comparator (`leanprover/comparator`)
2. Carlos Toledo, "Two claimed refutations of the Exponential Time Hypothesis: what was decided, and what was only read"