Weekly
News about Lean, the theorem prover and programming language.
Edition 18: 6 items published for May 28 to Jun 18, 2026.
Lean 4.31.0 lands 305 changes, including while let loops in do blocks, a built-in Lake linting framework, stricter transparency handling in definitional-equality checking, and the experimental mvcgen' tactic, which can outperform mvcgen by over 100x on some synthetic benchmarks. The bundled toolchain moves from LLVM 19 to LLVM 22.
Checked against: v4.31.0 release noteslean4 v4.31.0
Peter O'Hearn is hiring a postdoc in the Meta London office who will work closely with Peter O'Hearn and others in the new AI Verification team, collaborating across Meta Superintelligence Labs and possibly building on lean/CSLib, Iris-Lean and loom/velvet.
Checked against: LinkedIn post
A merged Lean 4 pull request by Wojciech Różowski makes the cbv tactic available inside grind's interactive sym => mode. The tactic reduces the goal using call-by-value evaluation, supports at locations for hypotheses, and closes equation goals via refl when reduction finishes the proof.
Checked against: lean4#13971
Pull request leanprover/lean4#12030, "feat: link OpenSSL" by Sofia Rodrigues, was merged on 2026-06-05. The pull request was opened on 2026-01-16 and describes its change as linking OpenSSL.
Checked against: lean4#12030
Quanta Books published The Proof in the Code on June 9, 2026, in which Kevin Hartnett tells the story of the birth and rise of Lean, from a bug-checking program at Microsoft Research developed by Leo de Moura to its adoption by mathematicians and tech firms.
Checked against: amazon.com
Software Foundations, a series of textbooks on formal proof and foundations of programming languages formalized in Rocq, is being translated to Lean for Fall courses at Penn and elsewhere. Benjamin Pierce says the team is ready to add a few people, especially educators, and will need alpha-testers later in the summer.
Checked against: leanprover.zulipchat.com