I currently 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.
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.