I work at Lean FRO on The Mathematical Workbench Project for the Lean 4 programming language and theorem prover.
Thanks to Alex Gerko from XTX Markets and all the Lean FRO sponsors and partners for making this project possible.
Verso Blueprint is a Lean package for writing structured proof blueprints in Verso. A blueprint connects mathematical exposition with Lean code and declarations, so a formalization plan can be read as a document and checked against the formal development.
It renders navigable HTML with previews, dependency graphs, progress summaries, and metadata for downstream tools.
lean-beam is a Claude/Codex skill and local workflow layer for efficient interaction with Lean 4, including experiments around proof-engine access and Monte-Carlo Tree Search.
lean-vir is a proof-of-concept path from Lean 4 IR to wasm32-wasi, useful for exploring how Lean programs and generated artifacts can move toward WebAssembly.
ml-lab is a Lean-first laboratory for OCaml bytecode and ZAM simulation, giving runtime and bytecode experiments a checked, programmable setting.
imp-lab is a Lean playground for programming-language modeling tooling, centered on small imperative languages and experiments around semantics.
lean-mirror packages Lean 4 language support for CodeMirror 6, with a thin LSP client layer, browser transports, and a small demo around lean --server.
Flèche is a new document processing engine for the Rocq Prover. Flèche is based on state-of-the-art incremental computing techniques and was designed to support real-time checking of hybrid and literate proof documents. Flèche is used, among others, in the following sub-projects that I also co-maintain:
rocq-lsp: a LSP server for the Rocq Prover.
jsCoq 2: interactive rich documents, run Rocq in your browser!
pétanque: lightweight programmatic interaction with the Rocq Prover.
Dune is an industrial-grade build system with great features and performance. We extended Dune to support Rocq projects, supporting most of Dune's key features such as caching and compositional builds. See Dune's Rocq Build Language Documentation for more details and a quick-start guide.
The Rocq Prover is an award-winning interactive theorem prover based on the Calculus of Constructions. I was a member of Rocq's core team from 2015 to 2025, helping co-maintain and design several components, including Rocq's build system, the vernacular layer, and the continuous integration system.