Earlier this year, Jakob von Raumer, Paul Reichert and I finished a long project adding the Freyd-Mitchell and Gabriel-Popescu theorems to mathlib, Lean’s mathematical library. This week, a blog post about the project went live on the Lean community blog. Click here to read it!| Markus Himmel
Lean 4.22 (to be released in early August) will ship with the first version of the new iterators library, allowing for efficient streaming, combining and collecting of data. This library was designed and implemented by Paul, and he has put a lot of thought into making sure that iterators are compiled into efficient code (like in Rust), and he has worked even harder to ensure that it’s easy to prove things about iterators (even when iterating monadically).| Markus Himmel
A few weeks ago I started the human-eval-lean project, an effort to collect hand-written solutions to the famous HumanEval (AI) programming benchmark, written in the programming language Lean. The twist is that Lean is not just a programming language, but also a proof assistant, and all solutions in human-eval-lean come with machine-checked formal proofs that the code is correct.| Markus Himmel
One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a first look at this feature, show a simple example of what it can do, and compare it to similar tools.| Markus Himmel