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