Floats in Lean 4.33
Here is a little informal Q&A-style post about the changes to Float in Lean 4.33. The questions are meant to be read from top to bottom, not in arbitrary...
Recent Posts
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...
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...