Mac Malone

lean4-alloy. Write C shims from within Lean code.

lean4-papyrus. An LLVM interface for Lean 4. (WIP)

lean4-partax. Lean 4 library of tools for parsing and compiling syntax and parser definitions.

lean4-itertools. A Lean 4 library for iterators.

leanpy. Python in Lean 4

folktale. Knights and Knaves logic puzzles formalized in Lean 4.

imperia. Experimenting with imperative programming in Lean

lyre. Lean IR as Lean syntax

lrt. Lean runtime formalization

lean-blake3. Lean4 bindings to the Blake3 (unfinished)