Toolchain pins leanprover/lean4:v4.33.0-rc1, which predates the kernel soundness fix for #14576

[morluto]

Summary

lean-toolchain pins leanprover/lean4:v4.33.0-rc1. That release candidate was tagged 2026-07-15, thirteen days before the kernel soundness fix for leanprover/lean4#14576 landed (PR #14577, merged 2026-07-28; shipped in nightly-2026-07-29 and the stable/patch releases v4.32.2 / v4.33.0 / v4.33.1).

The affected kernel accepts malformed nested-inductive declarations through the ordinary checked addDecl path and thereby an axiom-free proof of False (publicly demonstrated by the CollatzLean incident and the oss-security advisory, 2026-08-02). From False, any proposition — including the statements this repository certifies — is derivable.

Impact assessment for PrimeGapsLib

• Not a known exploit here: I audited the declaration-emitting code paths. The only raw addDecl uses emit .defnDecl/.thmDecl of natural-number literals, Lean.RArray trees, and reflBoolTrue proofs (PrimeGapsCert/Gap246/Emit/Commands.lean). There is no .inductDecl, no Expr.proj construction, no unsafe/native_decide/skipKernelTC, and no additional axioms anywhere in the repository. The bug does not affect arithmetic evaluation or the certificate computations themselves.
• Still a release blocker for a verification project: while the pinned kernel remains pre-fix, a green build cannot serve as an end-to-end soundness claim, because the trusted computing base contains a known-unsound component. Only a clean rebuild under a fixed kernel establishes that the proof does not depend on it.

Suggested remediation

1. Bump lean-toolchain to at least the fixed stable v4.33.0 (a Mathlib window built with it exists: mathlib@db584cd6, toolchain bump commit of 2026-08-10), moving the Mathlib pin in lockstep.
2. Rebuild all production targets from a clean .lake under the fixed toolchain.
3. Add independent verification to CI so regressions are caught mechanically: lean-action supports leanchecker: true, nanoda: true, nanoda-allow-sorry: false (all default to disabled today).
4. Longer term, prefer stable over RC toolchains for durable verification artifacts.

PR incoming.