This website is now powered by Verso

This website is now built with Verso, the documentation tool for Lean. Verso is developed by David Thrane Christiansen at the Lean FRO. It powers the Lean language reference manual, the Lean website, and now this site.

The main motivation: Lean code examples in blog posts are type-checked at build time and include interactive hover information. Try hovering over the code in Teaching AI to Make Proof Automation Work.

The site source is on GitHub. Each page is a .lean file. Blog posts and notes use Verso's markdown syntax inside #doc declarations. The site is built with lake build and deployed via GitHub Actions.