Week of Apr 9, 2026

Edition 12: 9 items published for Apr 2 to Apr 9, 2026.

Veil verifies distributed protocols with a framework embedded in Lean

Veil is an open-source multi-modal verification framework for distributed protocols, embedded in Lean. It combines symbolic and concrete model checking, SMT-based automated proofs, and interactive theorem proving in a single tool with foundational guarantees and in-editor feedback.

Checked against: lean-lang.org

Lean core Apr 9

Lean releases Nerodia, a work-in-progress library for writing Python modules in Lean

Nerodia is a library for Lean/Python FFI inspired by PyO3 that uses Lake, Lean's build system, and generates type stubs for editors. It has a very limited API and is released primarily as a proof-of-concept and to obtain feedback on its design and build process.

Checked against: leanprover/nerodia

Lean core Apr 9

Design note proposes a two-tier design for grind scalability

A HackMD note proposes to "separate the cheap default from the expensive exploration": a default grind mode that is cheap, fast and fails quickly, plus explicit named tactics such as nonlinear_ineqs and fin_cases that users, grind?, or AI invoke to produce replayable scripts.

grind scalability: Two-Tier design - HackMD — Image: hackmd.io

Checked against: hackmd.io

Lean core Apr 9

Verso Blueprint publishes FLT and Sphere Packing blueprints as reference ports

The leanprover/verso-blueprint package, for writing Blueprint documents in Verso, now publishes Verso ports of the FLT and Sphere Packing blueprints, while Noperthedron and Carleson sit outside the catalog on the retired 4.34 line. Emilio Jesús Gallego Arias's porting harness has a human use Codex CLI to carry out the porting work.

Checked against: leanprover/verso-blueprint ejgallego.github.io ejgallego/leanblueprint-to-verso

Lean core Apr 6

Leo de Moura merges Sym framework and transparency changes into Lean

Leo de Moura merged pull requests adding Sym.Arith infrastructure for arithmetic normalization, fixing the sym canonicalizer, and adding a backward.isDefEq.respectTransparency.types option. An opt-in linter also warns about rfl simp theorems that only hold at higher transparency, part of a broader effort to ensure isDefEq respects transparency levels.

Checked against: lean4#13289 lean4#13317 lean4#13280 lean4#13271 lean4#13272 lean4#13273 lean4#13281

Lean core Apr 5

Leo de Moura proposes stricter transparency default for Lean's definitional equality checker

Leo de Moura opened a pull request enabling the backward.isDefEq.respectTransparency.types option by default, so the definitional equality checker respects the current transparency setting when matching metavariable types. The change prevents unintended unfolding of definitions and requires adding @[implicit_reducible] and @[expose] attributes to many library definitions.

Checked against: lean4#13283

Lean core Mar 9

Kyle Miller merges Lean syntax and structure default value changes

In Lean, structure field defaults can now depend on fields that come before and after them, and dotted function notation supports explicit mode (@.f) and explicit universes (.f.{u,v}). Field notation such as e.f.{u,v} now also accepts explicit universe levels, fixing a bug where levels were attributed to the wrong expression.

Checked against: lean4#12841 lean4#13245 lean4#13262

Papers and events Apr 2

Leo de Moura explains in a blog post why Lean works

In "Why Lean?", dated 2026-04-02, Leo de Moura argues that implementing Lean in Lean lets users extend it freely, and points to a small trusted kernel with multiple independent implementations. The post also names backward compatibility as Lean's weakness: Lean code written two years ago probably needs changes to compile today.

Checked against: leodemoura.github.io

Papers and events Apr 9

Leo de Moura gives talk on Lean and machine-checked mathematics at SIMIS

Leo de Moura, Chief Architect of the Lean FRO, presented "Lean: Machine-Checked Mathematics" at the Shanghai Institute for Mathematics and Interdisciplinary Sciences (SIMIS) on April 7, 2026. The slides, written in Verso, cover AI provers that use Lean, Mathlib, and grind, a proof-automation tactic inspired by modern SMT solvers.

Checked against: leodemoura.github.io