My first verified (imperative) program
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 imperat...
Recent Posts
Freyd-Mitchell and Gabriel-Popescu Permalink
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 ma...
Lean has iterators now
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 col...
The largest divisor
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, writte...