The Lean Project Blog

Welcome to the Lean project's blog! Here, the core Lean developers will be posting announcements, tutorials, and other information that we think will be interesting to people who are not regular participants in the Lean Zulip chat.

This blog is implemented using Verso, the in-development documentation authoring tool for Lean. With Verso, each post is itself a Lean file. Indeed, every page on this site is a Lean file. An embedded DSL provides a Markdown-like notation, so writing documents in Lean is about as convenient as using an external authoring tool. However, the tight integration between documents and the Lean compiler makes it much easier to add documentation features that use the compiler's detailed understanding of programs.