2026-10-15 AI agents are very effective at finding vulnerabilities in our software. This includes the kernel (the proof checker) of the Lean proof assistant. See our two recent postmortems (August 1, August 24). We are strengthening the official kernel, adding new kernels, and building new tools that simplify rechecking your Lean developments with external kernels. Lean v4.35.0 comes with the lake check command. This command exports your development and rechecks it with leanchecker, the official...