My first verified (imperative) program
Important note: This post is out of date! It describes an old, early version of the mvcgen tactic. As of Lean 4.25.0, the syntax has changed a bit (for the b...
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...