9.6 Practices in other Lean projects

The mitigation and retirement plan follows several established patterns, without claiming that those projects have the same computational scale.

• Mathlib’s style linter flags native_decide because it trusts the compiler. The source explicitly calls this an incentive rather than a parser-level ban.

• PrimeCert uses external generation to provide data that Lean checks through proof-producing primality theorems. This is the desired architecture when a compact witness exists.

• LeanCert organizes computable data, a Boolean or exact checker, and a “golden theorem” connecting the checker to semantic mathematics. Its interfaces distinguish kernel and native closure and audit the resulting axioms. The family cards identify LeanCert tables or interval certificates as the main retirement route here.

• The PFR and FLT projects publish representative axiom output so that foundational dependencies remain reviewer-visible.

• Tools such as SafeVerify and ReplaceNativeDecide take the stricter policy of rejecting or attempting to replace native decisions. This repository’s –require-zero-native gate expresses the same end state while the documented production proof still contains large computations.