Po letech vývoje byl oficiálně vydán Lean 4. Jedná se o čistě funkcionální jazyk vycházející z ML.
Lean 4 má moderní syntaktické konstrukce, efektivní správu paměti (bez tracing GC) a jednoduché FFI pro nativní kód. Kód se překládá do C a následně spolu s runtimem do nativních binárek.