GoKawiilLean 4.35.0 adds lake check and four extra kernels including proven-consistent con-leche
The Lean proof assistant's new v4.35.0 release introduces a lake check command that re-verifies developments using leanchecker inside a sandbox, plus a --paranoid mode that runs four additional kernels: nanoda, lean4lean, con-leche, and con-ron. Con-leche, built in Lean itself by Claude models under supervision from Joachim Breitner at the Lean FRO, is formally proven consistent against a set-theoretic model and reportedly runs faster than the official kernel on the full Mathlib library.